impl preferred infoview

- add a setting for it - switch button of main toolbar to it
onriv · Nov 17, 2024 · 09021b1 · 09021b1
1 parent 0e121b2
commit 09021b1
Show file tree

Hide file tree

Showing 7 changed files with 139 additions and 41 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -6,6 +6,9 @@
 
 - add sdk and library support
 - add a soft wrap action/toolbar button for internal infoview
+- impl preferred infoview
+  - add a setting for it
+  - switch button of main toolbar to it
 
 ## [0.1.4] - 2024-11-11
 

diff --git a/README.md b/README.md
@@ -15,36 +15,53 @@ A [Lean4](https://lean-lang.org/) plugin for the Intellij Platform.
 
 # Installation
 
-This plugin uses [LSP4IJ](https://github.com/redhat-developer/lsp4ij) for connecting to the Lean4 language server. Please install that first.
+This plugin uses [LSP4IJ](https://github.com/redhat-developer/lsp4ij) for connecting to the Lean4 language server.
+Please install that first.
 
 - Using the IDE built-in plugin system: `Settings/Preferences` > `Plugins` > `Marketplace` > `Search for "lean4ij"` >
   `Install`
 
-- Manually: Download the [latest release](https://github.com/onriv/lean4ij/releases/latest) and install it manually using
-  `Settings/Preferences` > `Plugins` > `⚙️` > `Install plugin from disk...` For nightly builds go to [Actions/build](https://github.com/onriv/lean4ij/actions/workflows/build.yml), click the latest success run and scroll to the buttom.
+- Manually: Download the [latest release](https://github.com/onriv/lean4ij/releases/latest) and install it manually
+  using
+  `Settings/Preferences` > `Plugins` > `⚙️` > `Install plugin from disk...` For nightly builds go
+  to [Actions/build](https://github.com/onriv/lean4ij/actions/workflows/build.yml), click the latest success run and
+  scroll to the buttom.
 
-The plugin should be compatible from version 2024.1 and can not support the earlier versions for depending some experimental api)
+The plugin should be compatible from version 2024.1 and can not support the earlier versions for depending some
+experimental api)
 
 ## Usage
 
-For currently there is no functionality of creating a project or setting up a project. Before open any lean project with it please first testing if the project has set up the toolchain correctly. Run any command like `elan which lake` or `lake exe cache get`, or `lake build` etc.
+For currently there is no functionality of creating a project or setting up a project. Before open any lean project with
+it please first testing if the project has set up the toolchain correctly. Run any command like `elan which lake` or
+`lake exe cache get`, or `lake build` etc.
 
-The LSP server is start as any lean file is open in the Editor and the editor gets focus. If it not behaves correctly, try firing a restart action.
+The LSP server is start as any lean file is open in the Editor and the editor gets focus. If it not behaves correctly,
+try firing a restart action.
 
-Unicode is supported via live templates, for example typing `\b1<SPACE>` would result in `𝟙`. For the limitation of live templates, the `<SPACE>` keypress is always required.
+Unicode is supported via live templates, for example typing `\b1<SPACE>` would result in `𝟙`. For the limitation of live
+templates, the `<SPACE>` keypress is always required.
 
-Infoview is supported using [lean4-infoview,](https://github.com/leanprover/vscode-lean4/tree/master/lean4-infoview) and currently it can be started from a browser or the internal [JCEF]() infoview toolwindow. If it not behaves correctly, try firing a restart action too. There is also an infoview implemented in swing that's native
-in Jetbrains platform, it contains some basic functionally and for popup it requires a click.
+Infoview is supported using [lean4-infoview,](https://github.com/leanprover/vscode-lean4/tree/master/lean4-infoview) and
+currently it can be started from a browser or the internal [JCEF](https://plugins.jetbrains.com/docs/intellij/jcef.html)
+infoview toolwindow. If it not behaves correctly, try firing a restart action too. There is also an infoview implemented
+in swing that's native in Jetbrains platform, it contains some basic functionally. Currently, some terminologies are
+messed up here: all the terminologies like "jcef", "external", "browser", "vscode" refer to the first one and
+terminologies like "swing", "internal", "native" refer to the second one.
+
+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).
 
-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
 
-Currently, the following actions are defined, mostly without default shortcut. Add one for them in `Keymap` (like `Control Shift Enter` for toggle 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)                       |                  |  
+| ToggleLeanInfoViewInternal           | Lean4 Actions: Toggle Infoview (internal)                   |                  |  
+| ToggleLeanInfoViewJcef               | 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)    |                  |  
@@ -58,17 +75,21 @@ Currently, the following actions are defined, mostly without default shortcut. A
 ## Settings
 
 Since version 0.0.17 there are some settings available:
+
 - General setting is under `Settings/Preferences` > `Leanguages & Frameworks` > `Lean4`. Available settings are:
-  - (TODO) Enable Lsp Completion: Currently not support, waiting lsp4ij's new release. This is for currently discovering that sometimes lsp completion is slow. But it's enable by default.
+    - (TODO) Enable Lsp Completion: Currently not support, waiting lsp4ij's new release. This is for currently
+      discovering that sometimes lsp completion is slow. But it's enable by default.
 - Enable the native infoview, and timeout for popping the doc
 - Enable the external infoview
 - Extra css for external infoview. The most relevant I found is changing font-size
 
 The inlay hints related settings are under `Settings/Preferences` > `Inlay Hints` > `textmate`:
+
 - `Show inlay hint for omit type`
 - `Show value for placeholder _`
 
-Some color settings are under `Settings/Preferences` > `Editor` > `Color Scheme` >  `Lean Infoview`. It contains color settings for both the external and internal infoview.
+Some color settings are under `Settings/Preferences` > `Editor` > `Color Scheme` >  `Lean Infoview`. It contains color
+settings for both the external and internal infoview.
 
 <!-- Plugin description end -->
 
@@ -78,20 +99,28 @@ Please check [DEVELOP.md](./DEVELOP.md).
 
 ## Known Issues
 
-The plugin is still on an early stage, check [ISSUES.md](./ISSUES.md) for known and logged issues, and [TODO.md](./TODO.md)
+The plugin is still on an early stage, check [ISSUES.md](./ISSUES.md) for known and logged issues,
+and [TODO.md](./TODO.md)
 
 ## Troubleshooting
-- Currently, the plugin seems capable to open the same project with vscode in the same time (Although it may consume twice the cpu and memory resources). Try open the project simultaneously in VSC and JB-IDE while troubleshooting.
-- Currently, some log is printed in the build window for the progressing file and the url to the external/jcef infoview, if something does not work normally, some log there may help.
-- There are also detailed logs for the lsp server supported by LSP4IJ via the "language servers" tool window after setting the debug/trace level to verbose.
-- Some logs are also sent in the standard log file like `idea.log`. For different systems the path of it's the following paths, it can also be opened via `Help/Show log in ...` in the menu.
-  - (Linux) `$HOME.cache/JetBrains/<Product>/log/idea.log`
-  - (Windows) `$HOME\AppData\Local\JetBrains\<Product>\log\idea.log`
-  - (Macos) `~/Library/Caches/<Product>/log/idea.log`
+
+- Currently, the plugin seems capable to open the same project with vscode in the same time (Although it may consume
+  twice the cpu and memory resources). Try open the project simultaneously in VSC and JB-IDE while troubleshooting.
+- Currently, some log is printed in the build window for the progressing file and the url to the external/jcef infoview,
+  if something does not work normally, some log there may help.
+- There are also detailed logs for the lsp server supported by LSP4IJ via the "language servers" tool window after
+  setting the debug/trace level to verbose.
+- Some logs are also sent in the standard log file like `idea.log`. For different systems the path of it's the following
+  paths, it can also be opened via `Help/Show log in ...` in the menu.
+    - (Linux) `$HOME.cache/JetBrains/<Product>/log/idea.log`
+    - (Windows) `$HOME\AppData\Local\JetBrains\<Product>\log\idea.log`
+    - (Macos) `~/Library/Caches/<Product>/log/idea.log`
 - If the IDE is freezing, try check also the `threadDumps-freeze-***` files under the log folder.
 
-For showing debug/trace log, add `lean4ij:all` in `MENU > Help > Diagnostic Tools > Debug Log Settings` and restart, see [How-to-enable-debug-logging-in-IntelliJ-IDEA](https://youtrack.jetbrains.com/articles/SUPPORT-A-43/How-to-enable-debug-logging-in-IntelliJ-IDEA) for more docs.
-
+For showing debug/trace log, add `lean4ij:all` in `MENU > Help > Diagnostic Tools > Debug Log Settings` and restart,
+see [How-to-enable-debug-logging-in-IntelliJ-IDEA](https://youtrack.jetbrains.com/articles/SUPPORT-A-43/How-to-enable-debug-logging-in-IntelliJ-IDEA)
+for more docs.
+
 ## Acknowledgments
 
 The following projects give great help for developing the plugin:
@@ -114,4 +143,5 @@ and many source codes with references to
 Plugin based on the [IntelliJ Platform Plugin Template][template].
 
 [template]: https://github.com/JetBrains/intellij-platform-plugin-template
+
 [docs:plugin-description]: https://plugins.jetbrains.com/docs/intellij/plugin-user-experience.html#plugin-description-and-presentation
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.1.5-beta.0
+pluginVersion = 0.1.5-beta.1
 
 # 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/actions/ToggleLeanInfoViewInternal.kt b/src/main/kotlin/lean4ij/actions/ToggleLeanInfoViewInternal.kt
@@ -2,6 +2,7 @@ package lean4ij.actions
 
 import com.intellij.icons.AllIcons
 import com.intellij.ide.BrowserUtil
+import com.intellij.openapi.actionSystem.ActionManager
 import com.intellij.openapi.actionSystem.ActionUpdateThread
 import com.intellij.openapi.actionSystem.AnAction
 import com.intellij.openapi.actionSystem.AnActionEvent
@@ -18,6 +19,7 @@ import lean4ij.infoview.LeanInfoViewWindowFactory
 import lean4ij.infoview.LeanInfoviewService
 import lean4ij.infoview.external.JcefInfoviewService
 import lean4ij.infoview.external.JcefInfoviewTooWindowFactory
+import lean4ij.setting.Lean4Settings
 import lean4ij.util.LeanUtil
 import lean4ij.util.notify
 
@@ -58,15 +60,6 @@ class ToggleLeanInfoViewJcef : AnAction() {
         }
     }
 
-    override fun update(e: AnActionEvent) {
-        val editor = e.dataContext.getData<Editor>(CommonDataKeys.EDITOR)?:return
-        // TODO here it can be null, weird
-        val virtualFile = editor.virtualFile?: return
-        if (!LeanUtil.isLeanFile(editor.virtualFile)) {
-            e.presentation.isVisible = false
-        }
-    }
-
     override fun getActionUpdateThread(): ActionUpdateThread {
         return ActionUpdateThread.BGT;
     }
@@ -217,4 +210,33 @@ class ToggleInternalInfoviewSoftWrap : AbstractToggleUseSoftWrapsAction(SoftWrap
             }
         }
     }
+}
+
+class ToggleInfoviewPreferred : AnAction() {
+    private val lean4Settings = service<Lean4Settings>()
+    // TODO constant for the actions
+    private val toggleLeanInfoViewInternal = ActionManager.getInstance().getAction("ToggleLeanInfoViewInternal")
+    private val toggleLeanInfoViewJcef = ActionManager.getInstance().getAction("ToggleLeanInfoViewJcef")
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT;
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        when {
+            lean4Settings.preferredInfoview == "Jcef" ->
+                    toggleLeanInfoViewJcef.actionPerformed(e)
+            else ->
+                    toggleLeanInfoViewInternal.actionPerformed(e)
+        }
+    }
+
+    override fun update(e: AnActionEvent) {
+        val editor = e.dataContext.getData(CommonDataKeys.EDITOR)?:return
+        // TODO here it can be null, weird
+        val virtualFile = editor.virtualFile?: return
+        if (!LeanUtil.isLeanFile(virtualFile)) {
+            e.presentation.isVisible = false
+        }
+    }
 }
diff --git a/src/main/kotlin/lean4ij/setting/Lean4Configurable.kt b/src/main/kotlin/lean4ij/setting/Lean4Configurable.kt
@@ -7,9 +7,21 @@ import com.intellij.ui.components.JBCheckBox
 import com.intellij.ui.components.JBTextField
 import com.intellij.ui.dsl.builder.Panel
 import com.intellij.ui.dsl.builder.Row
+import java.awt.Component
+import javax.swing.DefaultListCellRenderer
 import javax.swing.JComponent
+import javax.swing.JList
 import kotlin.reflect.KMutableProperty0
 
+class ToolTipListCellRenderer(private val toolTips: List<String>) : DefaultListCellRenderer() {
+    override fun getListCellRendererComponent(list: JList<*>, value: Any?, index: Int, isSelected: Boolean, cellHasFocus: Boolean): Component {
+        val comp = super.getListCellRendererComponent(list, value, index, isSelected, cellHasFocus)
+        if (index >= 0 && index < toolTips.size) {
+            list.toolTipText = toolTips[index]
+        }
+        return comp
+    }
+}
 
 class Lean4SettingsView {
     private val lean4Settings = service<Lean4Settings>()
@@ -70,9 +82,10 @@ class Lean4SettingsView {
         cell(component).label(text)
     }
 
-    private val applyActions : MutableList<()->Unit> = mutableListOf()
-    private val resetActions : MutableList<()->Unit> = mutableListOf()
-    private val isChangedPredicates : MutableList<()->Boolean> = mutableListOf()
+    // TODO maybe it should not be public, but currently still no api for combos
+    val applyActions : MutableList<()->Unit> = mutableListOf()
+    val resetActions : MutableList<()->Unit> = mutableListOf()
+    val isChangedPredicates : MutableList<()->Boolean> = mutableListOf()
 }
 
 class Lean4Configurable : SearchableConfigurable {

diff --git a/src/main/kotlin/lean4ij/setting/Lean4Settings.kt b/src/main/kotlin/lean4ij/setting/Lean4Settings.kt
@@ -5,6 +5,7 @@ import com.intellij.openapi.components.Service
 import com.intellij.openapi.components.State
 import com.intellij.openapi.components.Storage
 import com.intellij.openapi.components.service
+import com.intellij.openapi.ui.ComboBox
 import com.intellij.ui.dsl.builder.panel
 import com.intellij.ui.layout.selected
 import com.intellij.util.xmlb.XmlSerializerUtil
@@ -39,6 +40,8 @@ class Lean4Settings : PersistentStateComponent<Lean4Settings> {
     var enableDiagnosticsLens = true
     var enableLspCompletion = true
 
+    // TODO this should switch to dropdown selection
+    var preferredInfoview = "Jcef"
     var enableNativeInfoview = true
     var autoUpdateInternalInfoview = true
     var hoveringTimeBeforePopupNativeInfoviewDoc = 200
@@ -98,11 +101,34 @@ fun Lean4SettingsView.createComponent(settings: Lean4Settings) = panel {
     group("Language Server Settings") {
         boolean("Enable language server", settings::enableLanguageServer)
         boolean("Enable the lean language server log (restart to take effect)", settings::enableLeanServerLog) {
-            comment("<a href='https://github.com/leanprover/lean4/tree/master/src/Lean/Server#in-general'>ref</a>")
+            comment("<a href='https://github.com/leanperrover/lean4/tree/master/src/Lean/Server#in-general'>ref</a>")
         }
         boolean("Enable lsp completion", settings::enableLspCompletion)
     }
     group("Infoview Settings") {
+
+        row {
+            val preferredInfoview = ComboBox(arrayOf(
+                "Jcef",
+                "Swing",
+                ))
+                .apply {
+                    renderer = ToolTipListCellRenderer(listOf("Prefer the Jcef/External/Vscode infoview", "Prefer the Swing/Native/Internal infoview"))
+                }
+            cell(preferredInfoview).label("Select preferred infoview")
+            applyActions.add {
+                preferredInfoview.selectedItem?.let {
+                    settings.preferredInfoview = it as String
+                }
+            }
+            resetActions.add {
+                preferredInfoview.selectedItem = settings.preferredInfoview
+            }
+            isChangedPredicates.add {
+                preferredInfoview.selectedItem != settings.preferredInfoview
+            }
+        }
+
         val (row, component) = boolean("Enable the native infoview", settings::enableNativeInfoview)
         boolean("Auto Update internal infoview", settings::autoUpdateInternalInfoview).let {
             val (row, _) = it

diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml
@@ -135,11 +135,15 @@
     <actions>
 
         <!-- infoview actions -->
-        <action id="OpenLeanInfoViewInternal" class="lean4ij.actions.ToggleLeanInfoViewInternal" text="Lean4 Actions: Toggle Infoview (internal) visibility" description="Lean4: Toggle Infoview (internal) visibility"
+        <action id="ToggleLeanInfoViewInternal" class="lean4ij.actions.ToggleLeanInfoViewInternal" text="Lean4 Actions: Toggle Infoview (internal) visibility" description="Lean4: Toggle Infoview (internal) visibility"
                 icon="/icons/infoview_icon.svg"
         >
         </action>
-        <action id="OpenLeanInfoViewJcef" class="lean4ij.actions.ToggleLeanInfoViewJcef" text="Lean4 Actions: Toggle Infoview (jcef) visibility" description="Lean4: Toggle Infoview (jcef) visibility"
+        <action id="ToggleLeanInfoViewJcef" class="lean4ij.actions.ToggleLeanInfoViewJcef" text="Lean4 Actions: Toggle Infoview (jcef) visibility" description="Lean4: Toggle Infoview (jcef) visibility"
+                icon="/icons/jcef_icon.svg"
+        >
+        </action>
+        <action id="ToggleInfoviewPreferred" class="lean4ij.actions.ToggleInfoviewPreferred" text="Lean4 Actions: Toggle Infoview (preferred) visibility" description="Lean4: Toggle Infoview (preferred) visibility"
                 icon="/icons/jcef_icon.svg"
         >
             <add-to-group group-id="MainToolbarRight" anchor="first"/>