add a soft wrap action/toolbar button for internal infoview

.run/MyPluginTest.run.xml

@@ -0,0 +1,19 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="MyPluginTest" type="JUnit" factoryName="JUnit" nameIsGenerated="true">
+    <module name="lean4ij.test" />
+    <extension name="coverage">
+      <pattern>
+        <option name="PATTERN" value="lean4ij.*" />
+        <option name="ENABLED" value="true" />
+      </pattern>
+    </extension>
+    <option name="PACKAGE_NAME" value="lean4ij" />
+    <option name="MAIN_CLASS_NAME" value="lean4ij.MyPluginTest" />
+    <option name="METHOD_NAME" value="" />
+    <option name="TEST_OBJECT" value="class" />
+    <option name="VM_PARAMETERS" value="--add-exports=java.base/jdk.internal.vm=ALL-UNNAMED --add-exports=java.base/sun.util.calendar=ALL-UNNAMED --add-exports=java.desktop/sun.awt=ALL-UNNAMED --add-exports=jdk.scripting.nashorn/jdk.nashorn.internal.ir=ALL-UNNAMED --add-opens=java.base/java.lang=ALL-UNNAMED --add-opens=java.base/java.lang.module=ALL-UNNAMED --add-opens=java.base/java.lang.reflect=ALL-UNNAMED --add-opens=java.base/java.math=ALL-UNNAMED --add-opens=java.base/java.nio=ALL-UNNAMED --add-opens=java.base/java.text=ALL-UNNAMED --add-opens=java.base/java.time=ALL-UNNAMED --add-opens=java.base/java.util=ALL-UNNAMED --add-opens=java.base/jdk.internal.jimage=ALL-UNNAMED --add-opens=java.base/jdk.internal.jimage.decompressor=ALL-UNNAMED --add-opens=java.base/jdk.internal.jrtfs=ALL-UNNAMED --add-opens=java.base/jdk.internal.loader=ALL-UNNAMED --add-opens=java.base/jdk.internal.math=ALL-UNNAMED --add-opens=java.base/jdk.internal.module=ALL-UNNAMED --add-opens=java.base/jdk.internal.perf=ALL-UNNAMED --add-opens=java.base/jdk.internal.platform.cgroupv1=ALL-UNNAMED --add-opens=java.base/jdk.internal.ref=ALL-UNNAMED --add-opens=java.base/jdk.internal.reflect=ALL-UNNAMED --add-opens=java.base/jdk.internal.util.jar=ALL-UNNAMED --add-opens=java.base/jdk.internal.vm=ALL-UNNAMED --add-opens=java.base/sun.nio.ch=ALL-UNNAMED --add-opens=java.desktop/com.apple.eawt=ALL-UNNAMED --add-opens=java.desktop/com.apple.eawt.event=ALL-UNNAMED --add-opens=java.desktop/com.apple.laf=ALL-UNNAMED --add-opens=java.desktop/java.awt=ALL-UNNAMED --add-opens=java.desktop/java.awt.dnd.peer=ALL-UNNAMED --add-opens=java.desktop/java.awt.event=ALL-UNNAMED --add-opens=java.desktop/java.awt.image=ALL-UNNAMED --add-opens=java.desktop/java.awt.peer=ALL-UNNAMED --add-opens=java.desktop/javax.swing=ALL-UNNAMED --add-opens=java.desktop/javax.swing.plaf.basic=ALL-UNNAMED --add-opens=java.desktop/javax.swing.text.html=ALL-UNNAMED --add-opens=java.desktop/sun.awt=ALL-UNNAMED --add-opens=java.desktop/sun.awt.image=ALL-UNNAMED --add-opens=java.desktop/sun.awt.windows=ALL-UNNAMED --add-opens=java.desktop/sun.font=ALL-UNNAMED --add-opens=java.desktop/sun.java2d=ALL-UNNAMED --add-opens=java.desktop/sun.lwawt=ALL-UNNAMED --add-opens=java.desktop/sun.lwawt.macosx=ALL-UNNAMED --add-opens=java.desktop/sun.swing=ALL-UNNAMED --add-opens=java.logging/sun.util.logging.internal=ALL-UNNAMED --add-opens=java.xml/javax.xml.catalog=ALL-UNNAMED --add-opens=java.xml/jdk.xml.internal=ALL-UNNAMED --add-opens=jdk.attach/sun.tools.attach=ALL-UNNAMED --add-opens=jdk.internal.jvmstat/sun.jvmstat.monitor=ALL-UNNAMED --add-opens=jdk.jdi/com.sun.tools.jdi=ALL-UNNAMED --add-opens=jdk.management/com.sun.management.internal=ALL-UNNAMED --add-opens=jdk.management.jfr/jdk.management.jfr=ALL-UNNAMED --add-opens=jdk.zipfs/jdk.nio.zipfs=ALL-UNNAMED -Didea.force.use.core.classloader=true -Djava.system.class.loader=com.intellij.util.lang.PathClassLoader -ea" />
+    <method v="2">
+      <option name="Make" enabled="true" />
+    </method>
+  </configuration>
+</component>

CHANGELOG.md

@@ -5,6 +5,7 @@
 ## [Unreleased]
 
 - add sdk and library support
+- add a soft wrap action/toolbar button for internal infoview
 
 ## [0.1.4] - 2024-11-11
 

DEVELOP.md

@@ -64,6 +64,72 @@ For first (and while require updating the frontend, run a `gradle buildBrowserIn
 
 # Debug and troubleshooting
 
+TODO
+
+# Test
+
+The unittests are essential for regression while refactoring the codebase and implementing new features. Although currently there is little tests wrote in the project.
+Running it from gradle seems working fine currently, but for running a selected test in Intellij, add the following vm options. Check some test configuration files in the
+`.run` directory for detail.
+
+```
+--add-exports=java.base/jdk.internal.vm=ALL-UNNAMED
+--add-exports=java.base/sun.util.calendar=ALL-UNNAMED
+--add-exports=java.desktop/sun.awt=ALL-UNNAMED
+--add-exports=jdk.scripting.nashorn/jdk.nashorn.internal.ir=ALL-UNNAMED
+--add-opens=java.base/java.lang=ALL-UNNAMED
+--add-opens=java.base/java.lang.module=ALL-UNNAMED
+--add-opens=java.base/java.lang.reflect=ALL-UNNAMED
+--add-opens=java.base/java.math=ALL-UNNAMED
+--add-opens=java.base/java.nio=ALL-UNNAMED
+--add-opens=java.base/java.text=ALL-UNNAMED
+--add-opens=java.base/java.time=ALL-UNNAMED
+--add-opens=java.base/java.util=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.jimage=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.jimage.decompressor=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.jrtfs=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.loader=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.math=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.module=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.perf=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.platform.cgroupv1=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.ref=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.reflect=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.util.jar=ALL-UNNAMED
+--add-opens=java.base/jdk.internal.vm=ALL-UNNAMED
+--add-opens=java.base/sun.nio.ch=ALL-UNNAMED
+--add-opens=java.desktop/com.apple.eawt=ALL-UNNAMED
+--add-opens=java.desktop/com.apple.eawt.event=ALL-UNNAMED
+--add-opens=java.desktop/com.apple.laf=ALL-UNNAMED
+--add-opens=java.desktop/java.awt=ALL-UNNAMED
+--add-opens=java.desktop/java.awt.dnd.peer=ALL-UNNAMED
+--add-opens=java.desktop/java.awt.event=ALL-UNNAMED
+--add-opens=java.desktop/java.awt.image=ALL-UNNAMED
+--add-opens=java.desktop/java.awt.peer=ALL-UNNAMED
+--add-opens=java.desktop/javax.swing=ALL-UNNAMED
+--add-opens=java.desktop/javax.swing.plaf.basic=ALL-UNNAMED
+--add-opens=java.desktop/javax.swing.text.html=ALL-UNNAMED
+--add-opens=java.desktop/sun.awt=ALL-UNNAMED
+--add-opens=java.desktop/sun.awt.image=ALL-UNNAMED
+--add-opens=java.desktop/sun.awt.windows=ALL-UNNAMED
+--add-opens=java.desktop/sun.font=ALL-UNNAMED
+--add-opens=java.desktop/sun.java2d=ALL-UNNAMED
+--add-opens=java.desktop/sun.lwawt=ALL-UNNAMED
+--add-opens=java.desktop/sun.lwawt.macosx=ALL-UNNAMED
+--add-opens=java.desktop/sun.swing=ALL-UNNAMED
+--add-opens=java.logging/sun.util.logging.internal=ALL-UNNAMED
+--add-opens=java.xml/javax.xml.catalog=ALL-UNNAMED
+--add-opens=java.xml/jdk.xml.internal=ALL-UNNAMED
+--add-opens=jdk.attach/sun.tools.attach=ALL-UNNAMED
+--add-opens=jdk.internal.jvmstat/sun.jvmstat.monitor=ALL-UNNAMED
+--add-opens=jdk.jdi/com.sun.tools.jdi=ALL-UNNAMED
+--add-opens=jdk.management/com.sun.management.internal=ALL-UNNAMED
+--add-opens=jdk.management.jfr/jdk.management.jfr=ALL-UNNAMED
+--add-opens=jdk.zipfs/jdk.nio.zipfs=ALL-UNNAMED
+-Didea.force.use.core.classloader=true
+-Djava.system.class.loader=com.intellij.util.lang.PathClassLoader
+-ea
+```
 
 
 # Ref

build.gradle.kts

@@ -80,6 +80,15 @@ dependencies {
         exclude("org.jetbrains.kotlinx", "kotlinx-coroutines-core")
         exclude("org.jetbrains.kotlinx", "kotlinx-coroutines-jdk8")
     }*/
+
+    /**
+     * In local unittest got the following error:
+     * Caused by: java.lang.ExceptionInInitializerError:
+     * Exception java.lang.UnsatisfiedLinkError:
+     * Native library (com/sun/jna/linux-x86-64/libjnidispatch.so) not found in resource path
+     * Hence add this, not saw before on GitHub action
+     */
+    testImplementation("net.java.dev.jna:jna:5.15.0")
 }
 
 // Set the JVM language level used to build the project.

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.4
+pluginVersion = 0.1.5-beta.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

src/main/kotlin/lean4ij/actions/RestartJcefInfoview.kt

@@ -7,11 +7,9 @@ import com.intellij.openapi.actionSystem.AnActionEvent
 import com.intellij.openapi.components.service
 import com.intellij.openapi.fileEditor.FileEditorManager
 import com.intellij.openapi.util.IconLoader.getIcon
-import com.intellij.ui.icons.getDisabledIcon
 import lean4ij.infoview.LeanInfoviewService
 import lean4ij.infoview.external.JcefInfoviewService
 import lean4ij.project.LeanProjectService
-import lean4ij.util.LeanUtil
 import javax.swing.Icon
 
 class RestartJcefInfoview : AnAction() {
@@ -43,6 +41,10 @@ class RestartInternalInfoview : AnAction() {
     override fun actionPerformed(e: AnActionEvent) {
         val project = e.project?:return
         FileEditorManager.getInstance(project).selectedTextEditor?.let { editor ->
+            // TODO here in fact message up two things:
+            //      one is recreating a new editor for removing old editor's bug
+            //      the other is updating infoview manually
+            project.service<LeanInfoviewService>().toolWindow?.restartEditor()
             project.service<LeanProjectService>().updateInfoviewFor(editor, true)
         }
     }

src/main/kotlin/lean4ij/actions/ToggleLeanInfoViewInternal.kt

@@ -8,7 +8,12 @@ import com.intellij.openapi.actionSystem.AnActionEvent
 import com.intellij.openapi.actionSystem.CommonDataKeys
 import com.intellij.openapi.components.service
 import com.intellij.openapi.editor.Editor
+import com.intellij.openapi.editor.actions.AbstractToggleUseSoftWrapsAction
+import com.intellij.openapi.editor.impl.softwrap.SoftWrapAppliancePlaces
 import com.intellij.openapi.util.IconLoader.getIcon
+import kotlinx.coroutines.TimeoutCancellationException
+import kotlinx.coroutines.runBlocking
+import kotlinx.coroutines.withTimeout
 import lean4ij.infoview.LeanInfoViewWindowFactory
 import lean4ij.infoview.LeanInfoviewService
 import lean4ij.infoview.external.JcefInfoviewService
@@ -179,4 +184,37 @@ class ToggleLeanInfoviewToolbarVisibility : AnAction() {
         component.isVisible = !component.isVisible
     }
 
+}
+
+/**
+ * TODO all the actions should be nicely grouped
+ *      ref: https://github.com/asciidoctor/asciidoctor-intellij-plugin/pull/222
+ */
+class ToggleInternalInfoviewSoftWrap : AbstractToggleUseSoftWrapsAction(SoftWrapAppliancePlaces.MAIN_EDITOR, false) {
+
+    init {
+        templatePresentation.icon = getIcon("/icons/newLine.svg", javaClass);
+
+        // TODO not sure if it should call the method copy from, but
+        //      it make the text into 'Soft-Wrap', which is wrong and cannot distinguish from the builtin action
+        // copyFrom(ActionManager.getInstance().getAction(IdeActions.ACTION_EDITOR_USE_SOFT_WRAPS));
+    }
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT;
+    }
+
+    override fun getEditor(e: AnActionEvent): Editor? {
+        val project = e.project ?: return null
+        val toolWindow = project.service<LeanInfoviewService>().toolWindow ?: return null
+        return runBlocking {
+            try {
+                withTimeout(1000) {
+                    toolWindow.getEditor()
+                }
+            } catch (ex: TimeoutCancellationException) {
+                null
+            }
+        }
+    }
 }

src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt

@@ -35,14 +35,23 @@ import javax.swing.JEditorPane
  */
 class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(true) {
     private val goals = JEditorPane()
-    val editor : CompletableDeferred<EditorEx> = CompletableDeferred()
+
+    /**
+     * TODO make this private
+     */
+    private val editor : CompletableDeferred<EditorEx> = CompletableDeferred()
+
+    suspend fun getEditor(): EditorEx {
+        return editor.await()
+    }
 
     /**
      * This si for displaying popup expr
      */
     val popupEditor : CompletableDeferred<EditorEx> = CompletableDeferred()
     val project = toolWindow.project
     val leanProject = project.service<LeanProjectService>()
+    val leanInfoviewService = project.service<LeanInfoviewService>()
     init {
         leanProject.scope.launch(Dispatchers.EDT) {
             try {
@@ -58,6 +67,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
                 popupEditor.completeExceptionally(ex)
             }
         }
+        leanInfoviewService.toolWindow = this
     }
 
     private val BORDER = BorderFactory.createEmptyBorder(3, 0, 5, 0)
@@ -117,7 +127,9 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
             }
             headerComponent = null
             setCaretEnabled(true)
-            setHorizontalScrollbarVisible(false)
+            // if true, then it's in fact also only visible if necessary
+            // check com.intellij.openapi.editor.impl.EditorImpl#setHorizontalScrollbarVisible
+            setHorizontalScrollbarVisible(true)
             setVerticalScrollbarVisible(true)
             isRendererMode = false
         }
@@ -195,4 +207,10 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
         editorEx.addEditorMouseMotionListener(mouseMotionListener!!)
     }
 
+    fun restartEditor() {
+        leanProject.scope.launch(Dispatchers.EDT) {
+            editor.complete(createEditor())
+        }
+    }
+
 }

src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt

@@ -211,6 +211,7 @@ class LeanInfoViewWindowFactory : ToolWindowFactory {
         // actions.add(manager.getAction("DecreaseZoomLevelForLeanInfoView"))
         // actions.add(manager.getAction("ResetZoomLevelForLeanInfoView"))
         actions.add(manager.getAction("ToggleLeanInfoviewToolbarVisibility"))
+        actions.add(manager.getAction("ToggleInternalInfoviewSoftWrap"))
 
         // TODO what is place for?
         val tb = manager.createActionToolbar("Lean Infoview", actions, true)

src/main/kotlin/lean4ij/infoview/LeanInfoviewService.kt

@@ -9,7 +9,7 @@ import com.intellij.openapi.project.Project
  */
 @Service(Service.Level.PROJECT)
 class LeanInfoviewService(private val project: Project) {
-
+   var toolWindow: LeanInfoViewWindow? = null
    var actionToolbar: ActionToolbar? = null
    var automaticallyRefreshInternalInfoview = true
 }

src/main/kotlin/lean4ij/sdk/Lean4StdLibraryProvider.kt

@@ -7,14 +7,19 @@ import java.nio.file.Files
 import java.nio.file.Path
 import kotlin.io.path.isDirectory
 import kotlin.io.path.name
+import kotlin.io.path.notExists
 
 /**
  * from julia-intellij, check src/org/ice1000/julia/lang/module/julia-sdks.kt
  */
 class Lean4StdLibraryProvider : AdditionalLibraryRootsProvider() {
     override fun getAdditionalProjectLibraries(project: Project): Collection<LeanLibrary> {
         val basePath = project.basePath ?: return listOf()
-        return Files.list(Path.of(basePath, ".lake", "packages"))
+        val packagesPath = Path.of(basePath, ".lake", "packages")
+        if (packagesPath.notExists()) {
+            return listOf()
+        }
+        return Files.list(packagesPath)
             .filter { it.isDirectory() }
             .map {
                 LeanLibrary(it.name, VfsUtil.findFile(it, true)!!)

src/main/resources/META-INF/plugin.xml

@@ -133,6 +133,8 @@
     </extensions>
 
     <actions>
+
+        <!-- infoview actions -->
         <action id="OpenLeanInfoViewInternal" class="lean4ij.actions.ToggleLeanInfoViewInternal" text="Lean4 Actions: Toggle Infoview (internal) visibility" description="Lean4: Toggle Infoview (internal) visibility"
                 icon="/icons/infoview_icon.svg"
         >
@@ -164,18 +166,17 @@
         <action id="OpenExternalInfoviewInBrowser" class="lean4ij.actions.OpenExternalInfoviewInBrowser" text="Lean4 Actions: Open infoview in browser" description="Lean4: Open infoview in browser">
             <add-to-group group-id="MainMenu" anchor="last"/>
         </action>
-        <action id="RestartLeanLsp" class="lean4ij.actions.RestartLeanLsp" text="Lean4 Actions: Restart Lean Lsp Server" description="Restart Lean Lsp Server">
-            <add-to-group group-id="MainMenu" anchor="last"/>
-        </action>
-        <action id="RestartCurrentLeanFile" class="lean4ij.actions.RestartCurrentFile" text="Lean4 Actions: Restart Current Lean File" description="Restart Current Lean File">
-            <add-to-group group-id="MainMenu" anchor="last"/>
-        </action>
         <action id="RestartJcefInfoview" class="lean4ij.actions.RestartJcefInfoview" text="Lean4 Actions: Restart Jcef Infoview" description="Lean4 Actions: Restart Jcef Infoview">
             <add-to-group group-id="MainMenu" anchor="last"/>
         </action>
         <action id="RestartInternalInfoview" class="lean4ij.actions.RestartInternalInfoview" text="Lean4 Actions: Restart Internal Infoview" description="Lean4 Actions: Restart Internal Infoview">
             <add-to-group group-id="MainMenu" anchor="last"/>
         </action>
+        <action id="ToggleInternalInfoviewSoftWrap" class="lean4ij.actions.ToggleInternalInfoviewSoftWrap" text="Lean4 Actions: Toggle Internal Infoview Soft Wrap" description="Lean4 Actions: Toggle Internal Infoview Soft Wrap">
+            <add-to-group group-id="MainMenu" anchor="last"/>
+        </action>
+
+        <!-- inlay hint actions -->
         <action id="AddInlayGoalHint" class="lean4ij.actions.AddInlayGoalHint" text="Lean4 Actions: Add Inlay Goal Hint" description="Add goal hint">
             <add-to-group group-id="CodeMenu" anchor="last"/>
             <keyboard-shortcut
@@ -191,6 +192,14 @@
             />
         </action>
 
+        <!-- lsp actions -->
+        <action id="RestartLeanLsp" class="lean4ij.actions.RestartLeanLsp" text="Lean4 Actions: Restart Lean Lsp Server" description="Restart Lean Lsp Server">
+            <add-to-group group-id="MainMenu" anchor="last"/>
+        </action>
+        <action id="RestartCurrentLeanFile" class="lean4ij.actions.RestartCurrentFile" text="Lean4 Actions: Restart Current Lean File" description="Restart Current Lean File">
+            <add-to-group group-id="MainMenu" anchor="last"/>
+        </action>
+
     </actions>
 
     <applicationListeners>