working on internal infoview popup doc window size

README.md

@@ -45,6 +45,21 @@ Messages and logs about the lean lsp server can be found in the language server
 | RestartCurrentLeanFile | Lean4 : Restart Current Lean File | restart current file        |
 | RestartJcefInfoview    | Lean4 : Restart Jcef Infoview     | restart the jcef infoview   |
 
+## 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.
+- 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.
+
 <!-- Plugin description end -->
 
 ## Development
@@ -56,13 +71,15 @@ Please check [DEVELOP.md](./DEVELOP.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`
-
+- If the IDE is freezing, try check also the `threadDumps-freeze-***` files under the log folder.
+
 ## Acknowledgments
 
 The following projects give great help for developing the plugin:

TODO.md

@@ -48,6 +48,7 @@
 - [ ] weird, is it just me or any other reason making only word autocompletion not working? In comment, it works but in normal pos it does not. It seems it's superseded by 
   some semantic autocompletion. --- yeah it's because semantic autocompletion is too slow. Can it be done in two steps? first show alphabet autocompletion and then add more semantic 
   autocompletion 
+- [ ] after bump lsp4ij to 0.7.0, make autocompletion configurable
 - [ ] quick fix for field missing
 - [x] color for error message
 - [ ] code completion seems slow and requires manually press ctrl+space
@@ -57,16 +58,24 @@
 – [x] two cases still exists for all messages: this should already be fixed
   1. it's not shown
   2. it's outdated
-– [x] some snippets to things like \<>
+– [x] some snippets to things like `\<>`
+- [ ] for some snippets maybe it's better to add a space, like `\to`, now for triggering it, it requires a space. But most case it will continue with a space.
+  - But not sure for the design, some absolutely don't want a auto created space
 – [ ] TODO weird brackets does not complete
 – [ ] maybe it's still better define some lang-like feature using parser/lexer, although it cannot be full parsed, but for the level like textmate it should be OK
 – [ ] is it possible do something like pygments/ctags/gtags completion?
 – [ ] option to skip library or backend files
 – [ ] error seems quite delay vanish... it shows errors event it has been fixed.
+- [ ] the internal infoview some case also delay (especially using ideavim one does not move caret)
 – [ ] comment auto comment like /-- trigger block comment
 – [ ] bock/line comment command
 – [ ] impl simp? which replace the code
 - [ ] settings for getAllMessages, both internal/external infoview
+- [ ] maybe it's just me with my idea settings, the gap between first column and line number is a little width
+- [ ] autogenerate missing fields
+- [ ] internal infoview when expanding all messages it seems jumping
+- [ ] check if live templates can dynamically define or not, in this way we can control if suffix space add automatically or not
+- [ ] internal infoview will automatically scroll to the end, kind of disturbing
 
 # Maybe some improvements
 

docs/inlayhints.md

@@ -0,0 +1,11 @@
+
+Some docs on positions that maybe enable inlay hints
+
+# instance field impl
+
+It seems useful with inlay hints at:
+
+```
+instance SomeImpl : SomeInst where
+  some_field /--add inlay hint here?-/:= 
+```

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

@@ -15,7 +15,6 @@ import com.intellij.openapi.vfs.VirtualFile
 import com.intellij.ui.awt.RelativePoint
 import com.intellij.ui.components.JBScrollPane
 import com.intellij.ui.components.panels.VerticalLayout
-import com.intellij.util.ui.JBFont
 import kotlinx.coroutines.CoroutineScope
 import kotlinx.coroutines.Dispatchers
 import kotlinx.coroutines.launch
@@ -30,10 +29,46 @@ import java.awt.Dimension
 import javax.swing.JEditorPane
 import javax.swing.JPanel
 import javax.swing.ScrollPaneConstants
+import kotlin.math.min
 
+/**
+ * Since currently we don't have a language implementation for the infoview, we cannot hover the content directly. Hence, we here implement a custom
+ * hovering logic for the infoview on infoview. Other reason is the vscode version infoview can hover on doc again and recursively. This is not supported by
+ * intellij idea (although intellij idea can open multiple docs in the documentation tool window, but ti's some kind not the same)
+ * TODO this is still very wrong, check [com.intellij.codeInsight.documentation.DocumentationScrollPane.setViewportView]
+ */
+class InfoviewPopupEditorPane(text: String, maxWidth: Int, maxHeight: Int) : JEditorPane() {
+
+    init {
+        val scheme = EditorColorsManager.getInstance().globalScheme
+        val schemeFont = scheme.getFont(EditorFontType.PLAIN)
+        contentType = "text/html"
+        // must add this, ref: https://stackoverflow.com/questions/12542733/setting-default-font-in-jeditorpane
+        putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES, true)
+        // TODO maybe some setting for this, font/size etc
+        font = schemeFont
+        this.text = text
+
+        // TODO this is still very wrong...
+        // It took me lots of time to handle the size...
+        // it turns out that the preferredSize should not be overridden or set at the beginning
+        // it should be called first to get some internal logic (quite complicated seems)
+        maximumSize = Dimension(maxWidth, Short.MAX_VALUE.toInt())
+        // // val width = Math.min(getPreferredContentWidth(doc.length), maxWidth)
+        // val width = maxWidth
+        // exprPane.size = Dimension(width, Short.MAX_VALUE.toInt())
+        val result = preferredSize
+        if (result.width > maxWidth) {
+            preferredSize = Dimension(maxWidth, min(maxHeight, result.height*(result.width/maxWidth+1)))
+        } else {
+            preferredSize = Dimension(result.width, result.height)
+        }
+
+    }
+}
 
 /**
- * TODO remove the internal api used here: DocumentationHtmlUtil.getDocPopupPreferredMinWidth()
+ * TODO this class absolutely need some refactor and a better implementation
  */
 class CodeWithInfosDocumentationHyperLink(
     val scope: CoroutineScope,
@@ -104,26 +139,9 @@ class CodeWithInfosDocumentationHyperLink(
 
     fun createDocPanel(doc: String): JEditorPane {
         val toolWindowSize = toolWindow.toolWindow.component.size
-        val scheme = EditorColorsManager.getInstance().globalScheme
-        val schemeFont = scheme.getFont(EditorFontType.PLAIN)
-        val docPanel = JEditorPane().apply {
-            contentType = "text/html"
-            // must add this, ref: https://stackoverflow.com/questions/12542733/setting-default-font-in-jeditorpane
-            putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES, true)
-            // TODO maybe some setting for this, font/size etc
-            font = JBFont.regular()
-            text = doc
-        }
-        // It took me lots of time to handle the size...
-        // it turns out that the preferredSize should not be overridden or set at the beginning
-        // it should be called first to get some internal logic (quite complicated seems)
         val maxWidth = toolWindowSize.width * 8 / 10
-        // TODO this uses internal ai
-        // val width = Math.min(getPreferredContentWidth(doc.length), maxWidth)
-        val width = maxWidth
-        docPanel.size = Dimension(width, Short.MAX_VALUE.toInt())
-        val result = docPanel.preferredSize
-        docPanel.preferredSize = Dimension(width, result.height)
+        val maxHeight = toolWindowSize.height * 8 / 10
+        val docPanel = InfoviewPopupEditorPane(doc, maxWidth, maxHeight)
         return docPanel
     }
 
@@ -133,31 +151,10 @@ class CodeWithInfosDocumentationHyperLink(
      * or use document directly
      */
     fun createExprPanel(typeAndExpr: String): JEditorPane {
-        // val editor = toolWindow.popupEditor.await()
-        val scheme = EditorColorsManager.getInstance().globalScheme
-        val schemeFont = scheme.getFont(EditorFontType.PLAIN)
-        var exprPane = JEditorPane().apply {
-            contentType = "text/html"
-            // must add this, ref: https://stackoverflow.com/questions/12542733/setting-default-font-in-jeditorpane
-            putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES, true)
-            // TODO maybe some setting for this, font/size etc
-            font = schemeFont
-            text = typeAndExpr
-        }
-
         val toolWindowSize = toolWindow.toolWindow.component.size
-        // It took me lots of time to handle the size...
-        // it turns out that the preferredSize should not be overridden or set at the beginning
-        // it should be called first to get some internal logic (quite complicated seems)
         val maxWidth = toolWindowSize.width * 8 / 10
-        exprPane.maximumSize = Dimension(maxWidth, Short.MAX_VALUE.toInt())
-        // // TODO this uses internal api
-        // // val width = Math.min(getPreferredContentWidth(doc.length), maxWidth)
-        // val width = maxWidth
-        // exprPane.size = Dimension(width, Short.MAX_VALUE.toInt())
-        // val result = exprPane.preferredSize
-        // exprPane.preferredSize = Dimension(width, result.height)
-
+        val maxHeight = toolWindowSize.height * 8 / 10
+        var exprPane = InfoviewPopupEditorPane(typeAndExpr, maxWidth, maxHeight)
         return exprPane
     }
 

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

@@ -144,6 +144,9 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru
         val editorEx: EditorEx = editor.await()
         editorEx.markupModel.removeAllHighlighters()
         editorEx.document.setText(interactiveInfo.toString())
+        // always move to the beginning while update goal, to avoid losing focus while all message expanded
+        // TODO nevertheless there maybe some better way
+        editorEx.caretModel.moveToOffset(0)
         editorEx.foldingModel.runBatchFoldingOperation {
             editorEx.foldingModel.clearFoldRegions()
             var allMessagesFoldRegion : FoldRegion? = null

src/main/resources/messages/MyBundle.properties

@@ -2,5 +2,5 @@ projectService=Project service: {0}
 randomLabel=The random number is: {0}
 shuffle=Shuffle
 notification.group.name=Lean Notification
-settings.lean.def.omit.type.name=Show inlay hint for omit type
-settings.lean.placeholder.value.name=Show value for placeholder _
+settings.lean.def.omit.type.name=Lean4: Show inlay hint for omit type
+settings.lean.placeholder.value.name=Lean4: Show value for placeholder _