release 0.1.0

onriv · Oct 27, 2024 · ccd03d7 · ccd03d7
1 parent 78741c1
commit ccd03d7
Show file tree

Hide file tree

Showing 5 changed files with 30 additions and 8 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -3,7 +3,8 @@
 # lean4ij Changelog
 
 ## [Unreleased]
-- register file type "lean4", dummy lexer/parser, temp icons (with the author's poor design skill) for toolwindow and file 
+- register file type "lean4", dummy lexer/parser (marked as 0.1.0 for this change)
+- temp icons (with the author's poor design skill) for toolwindow and file 
 - restricting scope for live templates to lean4
 - add commenter
 - actions for toggle infoview and open infoview in browser

diff --git a/README.md b/README.md
@@ -38,12 +38,21 @@ in Jetbrains platform, it contains some basic functionally and for popup it requ
 Messages and logs about the lean lsp server can be found in the language server tool window after setting the level to message or trace, check more information about this in [redhat-developer/lsp4ij](https://github.com/redhat-developer/lsp4ij).
 ### Actions
 
-| action id              | action text                       | meaning                     |
-|------------------------|-----------------------------------|-----------------------------|
-| OpenLeanInfoView       | Lean4 : Lean open info view       | open the infoview(swing)    |
-| RestartLeanLsp         | Lean4 : Restart Lean Lsp Server   | restart the  lsp server     |
-| RestartCurrentLeanFile | Lean4 : Restart Current Lean File | restart current file        |
-| RestartJcefInfoview    | Lean4 : Restart Jcef Infoview     | restart the jcef infoview   |
+Currently, the following actions are defined, mostly without default shortcut. Add one for them in `Keymap` (like `Control Shift Enter` for toggle infoview)
+
+| action id                            | action text                                                 | default shortcut |
+|--------------------------------------|-------------------------------------------------------------|------------------|
+| OpenLeanInfoViewInternal             | Lean4 Actions: Toggle Infoview (internal)                   |                  |  
+| OpenLeanInfoViewJcef                 | Lean4 Actions: Toggle Infoview (jcef)                       |                  |  
+| IncreaseZoomLevelForLeanInfoViewJcef | Lean4 Actions: Increase zoom level for lean infoview (jcef) |                  |  
+| DecreaseZoomLevelForLeanInfoViewJcef | Lean4 Actions: Decrease zoom level for lean infoview (jcef) |                  |  
+| ResetZoomLevelForLeanInfoViewJcef    | Lean4 Actions: Reset zoom level for lean infoview (jcef)    |                  |  
+| OpenExternalInfoviewInBrowser        | Lean4 Actions: Open infoview in browser                     |                  |  
+| RestartLeanLsp                       | Lean4 Actions: Restart Lean Lsp Server                      |                  |  
+| RestartCurrentLeanFile               | Lean4 Actions: Restart Current Lean File                    |                  |  
+| RestartJcefInfoview                  | Lean4 Actions: Restart Jcef Infoview                        |                  |  
+| AddInlayGoalHint                     | Lean4 Actions: Add Inlay Goal Hint                          | Control I        |  
+| DelInlayGoalHint                     | Lean4 Actions: Delete Inlay Goal Hint                       | Control Shift I  |  
 
 ## Settings
 
@@ -92,6 +101,15 @@ The following projects give great help for developing the plugin:
 - [leanprover-community/lean4-mode](https://github.com/leanprover-community/lean4-mode)
 - [redhat-developer/lsp4ij](https://github.com/redhat-developer/lsp4ij)
 
+and many source codes with references to
+
+- [intellij-arend](https://github.com/JetBrains/intellij-arend)
+- [intellij-haskell](https://github.com/rikvdkleij/intellij-haskell.git)
+- [julia-intellij](https://github.com/JuliaEditorSupport/julia-intellij)
+- [intellij-quarkus](https://github.com/redhat-developer/intellij-quarkus/)
+- [intellij-rust](https://github.com/intellij-rust/intellij-rust.git)
+- [intellij-sdk-code-samples](https://github.com/JetBrains/intellij-sdk-code-samples)
+
 Plugin based on the [IntelliJ Platform Plugin Template][template].
 
 [template]: https://github.com/JetBrains/intellij-platform-plugin-template

diff --git a/gradle.properties b/gradle.properties
@@ -5,7 +5,7 @@ pluginName = lean4ij
 pluginRepositoryUrl = https://github.com/onriv/lean4ij
 # SemVer format -> https://semver.org
 # TODO add sha1 to the beta output
-pluginVersion = 0.0.20.beta.4
+pluginVersion = 0.1.0
 
 # Supported build number ranges and IntelliJ Platform versions -> https://plugins.jetbrains.com/docs/intellij/build-number-ranges.html
 # For the dependence on textmate bundle api, the plugin must start build from 241

diff --git a/src/main/kotlin/lean4ij/language/InlayHints.kt b/src/main/kotlin/lean4ij/language/InlayHints.kt
@@ -286,6 +286,8 @@ class OmitTypeInlayHintsProvider : InlayHintsProvider {
     }
 
     override fun createCollector(file: PsiFile, editor: Editor): InlayHintsCollector? {
+        // TODO why here nullable?
+        if (file.virtualFile==null) return null
         return providers.computeIfAbsent(file.virtualFile.path) {
             OmitTypeInlayHintsCollector(editor, editor.project)
         }

diff --git a/src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt b/src/main/kotlin/lean4ij/lsp/data/CodeWithInfos.kt
@@ -118,6 +118,7 @@ class MsgEmbedGoal(val goal: InteractiveGoal) : MsgEmbed() {
 
     override fun contextInfo(offset: Int, startOffset: Int, endOffset : Int) : Triple<ContextInfo, Int, Int>? {
         // TODO when does this happen?
+        //      This happened on MIL/C07/S03_Subojects.lean:148
         TODO("Not yet implemented")
     }
 }