working on internal infoview trace

.run/GoalTest.testDeserializationLazyTraceChildrenToInteractiveResp.run.xml

@@ -0,0 +1,19 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="GoalTest.testDeserializationLazyTraceChildrenToInteractiveResp" type="JUnit" factoryName="JUnit" nameIsGenerated="true">
+    <module name="lean4ij.test" />
+    <extension name="coverage">
+      <pattern>
+        <option name="PATTERN" value="lean4ij.infoview.*" />
+        <option name="ENABLED" value="true" />
+      </pattern>
+    </extension>
+    <option name="PACKAGE_NAME" value="lean4ij.infoview" />
+    <option name="MAIN_CLASS_NAME" value="lean4ij.infoview.GoalTest" />
+    <option name="METHOD_NAME" value="testDeserializationLazyTraceChildrenToInteractiveResp" />
+    <option name="TEST_OBJECT" value="method" />
+    <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>

.run/GoalTest.testDeserializeLazyTraceChildrenToInteractiveResp.run.xml

@@ -0,0 +1,19 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="GoalTest.testDeserializeLazyTraceChildrenToInteractiveResp" type="JUnit" factoryName="JUnit" nameIsGenerated="true">
+    <module name="lean4ij.test" />
+    <extension name="coverage">
+      <pattern>
+        <option name="PATTERN" value="lean4ij.infoview.*" />
+        <option name="ENABLED" value="true" />
+      </pattern>
+    </extension>
+    <option name="PACKAGE_NAME" value="lean4ij.infoview" />
+    <option name="MAIN_CLASS_NAME" value="lean4ij.infoview.GoalTest" />
+    <option name="METHOD_NAME" value="testDeserializeLazyTraceChildrenToInteractiveResp" />
+    <option name="TEST_OBJECT" value="method" />
+    <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>

.run/GoalTest.testDeserializeMsgEmbedTrace.run.xml

@@ -0,0 +1,19 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="GoalTest.testDeserializeMsgEmbedTrace" type="JUnit" factoryName="JUnit" nameIsGenerated="true">
+    <module name="lean4ij.test" />
+    <extension name="coverage">
+      <pattern>
+        <option name="PATTERN" value="lean4ij.infoview.*" />
+        <option name="ENABLED" value="true" />
+      </pattern>
+    </extension>
+    <option name="PACKAGE_NAME" value="lean4ij.infoview" />
+    <option name="MAIN_CLASS_NAME" value="lean4ij.infoview.GoalTest" />
+    <option name="METHOD_NAME" value="testDeserializeMsgEmbedTrace" />
+    <option name="TEST_OBJECT" value="method" />
+    <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

@@ -9,7 +9,7 @@
   - a setting for the debouncing gap
 - some refactor on settings
 - setting for starting the language server eagerly or not
-- setting for file progressing all open editors eagerly or not (requires lsp 0.8.0)
+- setting for file progressing all open editors eagerly or not (requires lsp4ij 0.8.0)
 
 ## [0.1.5] - 2024-11-17
 

DEVELOP.md

@@ -51,7 +51,53 @@ the swing infoview is a raw infoview implemented using intellij platform's swing
 Currently, the code is still very badly organized for requiring further development.
 The entrance point for rendering is at `LeanFile.updateCaret` which call `LeanInfoViewWindowFactory.updateGoal` when all lsp call finish.
 
+### The design for `TaggedText` and `InfoViewContent`
 
+The implementation for the internal infoview, especially the render part needs big refactor.
+
+Currently, the design for `TaggedText` and `InfoviewContent` is extremely complicated for not sure what the contract is. 
+
+The generic class `TaggedText` is original designed for respecting the following structure in the lean source code `src/Lean/Widget/TaggedText.lean`.
+
+```lean4
+inductive TaggedText (α : Type u) where
+  | text   : String → TaggedText α
+  /-- Invariants:
+  - non-empty
+  - no adjacent `text` elements (they should be collapsed)
+  - no directly nested `append`s (but `append #[tag _ (append ..)]` is okay) -/
+  | append : Array (TaggedText α) → TaggedText α
+  | tag    : α → TaggedText α → TaggedText α
+```
+
+That has three constructors. Here they are represented in three subclass: `TaggedTextText`, `TaggedTextAppend` and `TaggedTextTag`.
+For the type α in the above lean source code, currently it's the interface `InfoViewContent` and the implementations are
+- SubexprInfo
+- MsgEmbed
+  - MsgEmbedExpr
+  - MsgEmbedGoal
+  - MsgEmbedTrace
+  - MsgUnsupported
+
+The implementation `SubexprInfo` corresponds to the following source code in the lean4 codebase in `Lean/Widget/InteractiveCode.lean` and is used for
+displaying interactive goals/expecting types in the infoview:
+
+```lean4
+structure SubexprInfo where
+  /-- The `Elab.Info` node with the semantics of this part of the output. -/
+  info : WithRpcRef Lean.Elab.InfoWithCtx
+  /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/
+  subexprPos : Lean.SubExpr.Pos
+  -- TODO(WN): add fields for semantic highlighting
+  -- kind : Lsp.SymbolKind
+  /-- In certain situations such as when goal states change between positions in a tactic-mode proof,
+  we can show subexpression-level diffs between two expressions. This field asks the renderer to
+  display the subexpression as in a diff view (e.g. red/green like `git diff`). -/
+  diffStatus? : Option DiffTag := none
+  deriving RpcEncodable
+```
+
+The `MsgEmbed` and its subclasses are used for displaying the messages. Almost all complexities came from this part.
 
 ## Developing in Intellij Idea
  Proxy issue (this should only happen in some specific region)

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

@@ -0,0 +1,28 @@
+package lean4ij.infoview
+
+import com.intellij.openapi.editor.event.EditorMouseEvent
+import com.intellij.openapi.editor.event.EditorMouseListener
+import lean4ij.lsp.data.InfoviewRender
+
+class InfoviewMouseListener(private val infoviewRender: InfoviewRender) : EditorMouseListener {
+
+    override fun mousePressed(event: EditorMouseEvent) {
+        super.mousePressed(event)
+    }
+
+    override fun mouseClicked(event: EditorMouseEvent) {
+        infoviewRender.getClickAction(event.offset)?.invoke(event)
+    }
+
+    override fun mouseReleased(event: EditorMouseEvent) {
+        super.mouseReleased(event)
+    }
+
+    override fun mouseEntered(event: EditorMouseEvent) {
+        super.mouseEntered(event)
+    }
+
+    override fun mouseExited(event: EditorMouseEvent) {
+        super.mouseExited(event)
+    }
+}

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

@@ -142,7 +142,7 @@ class InfoviewPopupDocumentation(
             )
             val infoToInteractive = leanProjectService.languageServer.await()
                 .infoToInteractive(rpcParams)
-            val sb = InfoviewRender()
+            val sb = InfoviewRender(project, file)
             val typeStr = infoToInteractive.type?.toInfoViewString(sb, null) ?: ""
             val exprStr = infoToInteractive.exprExplicit?.toInfoViewString(sb, null) ?: ""
             var htmlDoc: String? = null

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

@@ -6,8 +6,8 @@ import com.intellij.openapi.application.EDT
 import com.intellij.openapi.components.service
 import com.intellij.openapi.editor.EditorFactory
 import com.intellij.openapi.editor.FoldRegion
-import com.intellij.openapi.editor.LogicalPosition
 import com.intellij.openapi.editor.ScrollType
+import com.intellij.openapi.editor.event.EditorMouseListener
 import com.intellij.openapi.editor.event.EditorMouseMotionListener
 import com.intellij.openapi.editor.ex.EditorEx
 import com.intellij.openapi.editor.ex.FoldingListener
@@ -145,11 +145,12 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
     }
 
     private var mouseMotionListener : EditorMouseMotionListener? = null
+    private var mouseListener : EditorMouseListener? = null
     /**
      *  // TODO this should add some UT for the rendering
      */
     suspend fun updateEditorMouseMotionListener(
-        interactiveInfo: InfoviewRender,
+        infoviewRender: InfoviewRender,
         file: VirtualFile,
         position: Position,
         interactiveGoals: InteractiveGoals?,
@@ -159,7 +160,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
     ) {
         val editorEx: EditorEx = editor.await()
         editorEx.markupModel.removeAllHighlighters()
-        editorEx.document.setText(interactiveInfo.toString())
+        editorEx.document.setText(infoviewRender.toString())
 
         // TODO maybe a configuration for this
         // always move to the beginning while update goal, to avoid losing focus while all message expanded
@@ -170,7 +171,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
         editorEx.foldingModel.runBatchFoldingOperation {
             editorEx.foldingModel.clearFoldRegions()
             var allMessagesFoldRegion : FoldRegion? = null
-            for (folding in interactiveInfo.foldings) {
+            for (folding in infoviewRender.foldings) {
                 val foldRegion = editorEx.foldingModel.addFoldRegion(folding.startOffset, folding.endOffset, folding.placeholderText)
                 foldRegion?.isExpanded = folding.expanded
                 if (folding.isAllMessages) {
@@ -188,7 +189,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
             }
         }
         // highlights
-        for (highlight in interactiveInfo.highlights) {
+        for (highlight in infoviewRender.highlights) {
             editorEx.markupModel.addRangeHighlighter(highlight.startOffset, highlight.endOffset, HighlighterLayer.SYNTAX, highlight.textAttributes, HighlighterTargetArea.EXACT_RANGE)
         }
 
@@ -202,9 +203,16 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
         if (mouseMotionListener != null) {
             editorEx.removeEditorMouseMotionListener(mouseMotionListener!!)
         }
+        // TODO this can be refactored to the InfoviewRender class, in that way the definition of hovering
+        //      can be done in the same time when the rendering is defined
         mouseMotionListener = InfoviewMouseMotionListener(leanProject, this, editorEx, file, position,
             interactiveGoals, interactiveTermGoal, interactiveDiagnostics, interactiveDiagnosticsAllMessages)
         editorEx.addEditorMouseMotionListener(mouseMotionListener!!)
+        if (mouseListener != null) {
+            editorEx.removeEditorMouseListener(mouseListener!!)
+        }
+        mouseListener = InfoviewMouseListener(infoviewRender)
+        editorEx.addEditorMouseListener(mouseListener!!)
     }
 
     fun restartEditor() {

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

@@ -73,7 +73,7 @@ class LeanInfoViewWindowFactory : ToolWindowFactory {
             }
             val infoViewWindow = getLeanInfoview(project) ?: return
             // TODO implement the fold/open logic
-            val infoviewRender = InfoviewRender()
+            val infoviewRender = InfoviewRender(project, file)
             val start = infoviewRender.length
             val header = "${file.name}:${position.line+1}:${position.character}"
             infoviewRender.append("${header}")