diff --git a/CHANGELOG.md b/CHANGELOG.md index 3fcff92..7e892fd 100644 --- 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 index 5b26bed..20400ca 100644 --- 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 index 3eae0d6..45b390f 100644 --- 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 index 843f665..fe1c8b0 100644 --- 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 index 587dcad..efb2363 100644 --- 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") } }