Merge pull request #73 from onriv/feat/internal_infoview_trace

internal infoview trace
onriv · Dec 1, 2024 · 26612ab · 26612ab
2 parents 8c6ac65 + 410c365
commit 26612ab
Show file tree

Hide file tree

Showing 37 changed files with 3,633 additions and 119 deletions.
diff --git a/.run/GoalTest.run.xml b/.run/GoalTest.run.xml
@@ -0,0 +1,19 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="GoalTest" 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="" />
+    <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>
diff --git a/.run/GoalTest.testDeserializationLazyTraceChildrenToInteractiveResp.run.xml b/.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>
diff --git a/.run/GoalTest.testDeserializeLazyTraceChildrenToInteractiveResp.run.xml b/.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>
diff --git a/.run/GoalTest.testDeserializeMsgEmbedTrace.run.xml b/.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>
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -3,6 +3,8 @@
 # lean4ij Changelog
 
 ## [Unreleased]
+- refactoring the internal infoview, and
+- add a first implementation for trace message in internal infoview
 
 ## [0.1.6] - 2024-11-25
 

diff --git a/DEVELOP.md b/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)

diff --git a/src/main/kotlin/lean4ij/infoview/InfoviewMouseListener.kt b/src/main/kotlin/lean4ij/infoview/InfoviewMouseListener.kt
@@ -0,0 +1,51 @@
+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)
+    }
+}
+
+class InfoviewMouseListenerV1(private val context: LeanInfoviewContext) : EditorMouseListener {
+
+    override fun mousePressed(event: EditorMouseEvent) {
+        super.mousePressed(event)
+    }
+
+    override fun mouseClicked(event: EditorMouseEvent) {
+        context.rootObjectModel.getChild(event.offset)?.click(context)
+    }
+
+    override fun mouseReleased(event: EditorMouseEvent) {
+        super.mouseReleased(event)
+    }
+
+    override fun mouseEntered(event: EditorMouseEvent) {
+        super.mouseEntered(event)
+    }
+
+    override fun mouseExited(event: EditorMouseEvent) {
+        super.mouseExited(event)
+    }
+}
diff --git a/src/main/kotlin/lean4ij/infoview/InfoviewMouseMotionListener.kt b/src/main/kotlin/lean4ij/infoview/InfoviewMouseMotionListener.kt
@@ -2,7 +2,6 @@ package lean4ij.infoview
 
 import com.intellij.execution.impl.EditorHyperlinkSupport
 import com.intellij.openapi.components.service
-import com.intellij.openapi.editor.LogicalPosition
 import com.intellij.openapi.editor.colors.CodeInsightColors
 import com.intellij.openapi.editor.colors.EditorColors
 import com.intellij.openapi.editor.colors.EditorColorsManager
@@ -19,13 +18,13 @@ import kotlinx.coroutines.TimeoutCancellationException
 import kotlinx.coroutines.channels.Channel
 import kotlinx.coroutines.launch
 import kotlinx.coroutines.withTimeout
-import lean4ij.setting.Lean4Settings
 import lean4ij.lsp.data.ContextInfo
 import lean4ij.lsp.data.InteractiveDiagnostics
 import lean4ij.lsp.data.InteractiveGoals
 import lean4ij.lsp.data.InteractiveTermGoal
 import lean4ij.lsp.data.Position
 import lean4ij.project.LeanProjectService
+import lean4ij.setting.Lean4Settings
 import java.awt.Color
 
 /**