From 145ab9eae5a5b4c052d8f9c4dca94770cff6239b Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Fri, 11 Oct 2024 01:13:24 +0800 Subject: [PATCH 01/11] working on internal infoview popup doc window size --- README.md | 19 ++++- TODO.md | 11 ++- docs/inlayhints.md | 11 +++ .../CodeWithInfosDocumentationHyperLink.kt | 85 +++++++++---------- .../lean4ij/infoview/LeanInfoViewWindow.kt | 3 + .../resources/messages/MyBundle.properties | 4 +- 6 files changed, 85 insertions(+), 48 deletions(-) create mode 100644 docs/inlayhints.md diff --git a/README.md b/README.md index 5f689de7..0512aa6b 100644 --- a/README.md +++ b/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. + ## 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//log/idea.log` - (Windows) `$HOME\AppData\Local\JetBrains\\log\idea.log` - (Macos) `~/Library/Caches//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: diff --git a/TODO.md b/TODO.md index e2255c98..7e755855 100644 --- a/TODO.md +++ b/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 diff --git a/docs/inlayhints.md b/docs/inlayhints.md new file mode 100644 index 00000000..72738bee --- /dev/null +++ b/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?-/:= +``` \ No newline at end of file diff --git a/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt b/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt index 9463c934..753ac489 100644 --- a/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt +++ b/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 } diff --git a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt index 4b347441..da638b88 100644 --- a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt +++ b/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 diff --git a/src/main/resources/messages/MyBundle.properties b/src/main/resources/messages/MyBundle.properties index 5bf779a2..44fcf8a2 100644 --- a/src/main/resources/messages/MyBundle.properties +++ b/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 _ \ No newline at end of file +settings.lean.def.omit.type.name=Lean4: Show inlay hint for omit type +settings.lean.placeholder.value.name=Lean4: Show value for placeholder _ \ No newline at end of file From 86932898951d5332c7cf13ef88c015da732d2429 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Fri, 11 Oct 2024 10:40:44 +0800 Subject: [PATCH 02/11] Update gradle.properties --- gradle.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gradle.properties b/gradle.properties index 8fa494d7..a199e3c7 100644 --- a/gradle.properties +++ b/gradle.properties @@ -4,7 +4,7 @@ pluginGroup = lean4ij pluginName = lean4ij pluginRepositoryUrl = https://github.com/onriv/lean4ij # SemVer format -> https://semver.org -pluginVersion = 0.0.17 +pluginVersion = 0.0.18.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 From 50fd4d9c65792a397a294330df1c0ee422622fc4 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Fri, 11 Oct 2024 10:45:52 +0800 Subject: [PATCH 03/11] Update CHANGELOG.md --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a235e80f..510cae8c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3,7 +3,7 @@ # lean4ij Changelog ## [Unreleased] - +- fix caret of internal infoview at first line first col while refreshing ## [0.0.17] - 2024-10-06 Depend on the latest approved nightly build of LSP4IJ: 0.7.0-20241006-013203 From ff9869cc45e2986d49a5c04130103c38bc8e28db Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Fri, 11 Oct 2024 12:37:47 +0800 Subject: [PATCH 04/11] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0512aa6b..ca5f9ad2 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ This plugin uses [LSP4IJ](https://github.com/redhat-developer/lsp4ij) for connec `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...` + `Settings/Preferences` > `Plugins` > `⚙️` > `Install plugin from disk...` For nightly builds go to [Actions/build](https://github.com/onriv/lean4ij/actions/workflows/build.yml) and download from the buttom of eachsuccess run. The plugin should be compatible from version 2024.1 and can not support the earlier versions for depending on textmate plugin's extension api. ## Usage From 90f3096c3f7c2faf9f18a1f21c2a13db8a56668e Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Sun, 13 Oct 2024 12:18:00 +0800 Subject: [PATCH 05/11] working on internal infoview popup doc window size --- src/main/kotlin/lean4ij/Lean4Configurable.kt | 142 ++++++++++++++---- .../CodeWithInfosDocumentationHyperLink.kt | 105 ++++++++----- 2 files changed, 184 insertions(+), 63 deletions(-) diff --git a/src/main/kotlin/lean4ij/Lean4Configurable.kt b/src/main/kotlin/lean4ij/Lean4Configurable.kt index 418818de..b7c2e878 100644 --- a/src/main/kotlin/lean4ij/Lean4Configurable.kt +++ b/src/main/kotlin/lean4ij/Lean4Configurable.kt @@ -55,7 +55,13 @@ fun Panel.checked(checkBox: AbstractButton, component: T, init: class ToolTipListCellRenderer(private val toolTips: List) : DefaultListCellRenderer() { - override fun getListCellRendererComponent(list: JList<*>, value: Any?, index: Int, isSelected: Boolean, cellHasFocus: Boolean): Component { + 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] @@ -76,10 +82,16 @@ class Lean4Settings : PersistentStateComponent { var enableNativeInfoview = true var hoveringTimeBeforePopupNativeInfoviewDoc = 200 + var nativeInfoviewPopupMinWidthTextLengthUpperBound = 200 + var nativeInfoviewPopupMaxWidthTextLengthLowerBound = 1000 + var nativeInfoviewPopupPreferredMinWidth = 500 + var nativeInfoviewPopupPreferredMaxWidth = 800 + var disableNativeInfoviewUpdateAtWindowClosed = false var enableVscodeInfoview = true var disableVscodeInfoviewUpdateAtWindowClosed = false var enableExtraCssForVscodeInfoview = false + // TODO this function should not be ref here, but move it to here and ref it from the infoview package maybe var extraCssForVscodeInfoview = createThemeCss(EditorColorsManager.getInstance().globalScheme) @@ -102,6 +114,9 @@ data class Lean4SettingsState( val extraCssForVscodeInfoview: String, ) +/** + * TODO adding setting is cumbersome, check if it's any better way to do it + */ class Lean4SettingsView { private val lean4Settings = service() @@ -109,14 +124,33 @@ class Lean4SettingsView { // Infoview settings private val enableNativeInfoview = JBCheckBox("Enable the native infoview", lean4Settings.enableNativeInfoview) - private val hoveringTimeBeforePopupNativeInfoviewDoc = JBIntSpinner(lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc, 50, 3000) + private val hoveringTimeBeforePopupNativeInfoviewDoc = + JBIntSpinner(lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc, 50, 3000) + private val nativeInfoviewPopupMinWidthTextLengthUpperBound = + JBIntSpinner(lean4Settings.nativeInfoviewPopupMinWidthTextLengthUpperBound, 0, 3000) + private val nativeInfoviewPopupMaxWidthTextLengthLowerBound = + JBIntSpinner(lean4Settings.nativeInfoviewPopupMaxWidthTextLengthLowerBound, 0, 3000) + private val nativeInfoviewPopupPreferredMinWidth = + JBIntSpinner(lean4Settings.nativeInfoviewPopupPreferredMinWidth, 0, 3000) + private val nativeInfoviewPopupPreferredMaxWidth = + JBIntSpinner(lean4Settings.nativeInfoviewPopupPreferredMaxWidth, 0, 3000) + // TODO - private val disableNativeInfoviewUpdateAtWindowClosed = JBCheckBox("Disable native infoview update at tool window closed", lean4Settings.disableNativeInfoviewUpdateAtWindowClosed) + private val disableNativeInfoviewUpdateAtWindowClosed = JBCheckBox( + "Disable native infoview update at tool window closed", + lean4Settings.disableNativeInfoviewUpdateAtWindowClosed + ) + // TODO private val enableVscodeInfoview = JBCheckBox("Enable the vscode infoview", lean4Settings.enableVscodeInfoview) + // TODO - private val disableVscodeInfoviewUpdateAtWindowClosed = JBCheckBox("Disable vscode infoview update at tool window closed", lean4Settings.disableVscodeInfoviewUpdateAtWindowClosed) - private val enableExtraCssForVscodeInfoview = JBCheckBox("Enable extra css for vscode infoview", lean4Settings.enableExtraCssForVscodeInfoview) + private val disableVscodeInfoviewUpdateAtWindowClosed = JBCheckBox( + "Disable vscode infoview update at tool window closed", + lean4Settings.disableVscodeInfoviewUpdateAtWindowClosed + ) + private val enableExtraCssForVscodeInfoview = + JBCheckBox("Enable extra css for vscode infoview", lean4Settings.enableExtraCssForVscodeInfoview) /** * copy from [com.intellij.ui.dsl.builder.impl.RowImpl.textArea] @@ -144,23 +178,38 @@ class Lean4SettingsView { private fun setExtraCssForTextAreaIsEditable(isEditable: Boolean) { extraCssForVscodeInfoview.isEditable = isEditable if (!isEditable) { - extraCssForVscodeInfoview.background = EditorColorsManager.getInstance().globalScheme.getAttributes(DefaultLanguageHighlighterColors.LINE_COMMENT).backgroundColor + extraCssForVscodeInfoview.background = + EditorColorsManager.getInstance().globalScheme.getAttributes(DefaultLanguageHighlighterColors.LINE_COMMENT).backgroundColor } else { - extraCssForVscodeInfoview.background = EditorColorsManager.getInstance().globalScheme.getAttributes(HighlighterColors.TEXT).backgroundColor + extraCssForVscodeInfoview.background = + EditorColorsManager.getInstance().globalScheme.getAttributes(HighlighterColors.TEXT).backgroundColor } } - val isModified: Boolean get() { - val enableNativeInfoviewChanged = enableNativeInfoview.isSelected != lean4Settings.enableNativeInfoview - val enableVscodeInfoviewChanged = enableVscodeInfoview.isSelected != lean4Settings.enableVscodeInfoview - val enableExtraCssForVscodeInfoviewChanged = enableExtraCssForVscodeInfoview.isSelected != lean4Settings.enableExtraCssForVscodeInfoview - val extraCssForVscodeInfoviewChanged = extraCssForVscodeInfoview.text != lean4Settings.extraCssForVscodeInfoview - val hoveringTimeBeforePopupNativeInfoviewDocChanged = hoveringTimeBeforePopupNativeInfoviewDoc.number != lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc - var enableLspCompletionChanged = enableLspCompletion.isSelected != lean4Settings.enableLspCompletion - return enableNativeInfoviewChanged || enableVscodeInfoviewChanged || enableExtraCssForVscodeInfoviewChanged || - extraCssForVscodeInfoviewChanged || hoveringTimeBeforePopupNativeInfoviewDocChanged || enableLspCompletionChanged - - } + val isModified: Boolean + get() { + val enableNativeInfoviewChanged = enableNativeInfoview.isSelected != lean4Settings.enableNativeInfoview + val enableVscodeInfoviewChanged = enableVscodeInfoview.isSelected != lean4Settings.enableVscodeInfoview + val enableExtraCssForVscodeInfoviewChanged = + enableExtraCssForVscodeInfoview.isSelected != lean4Settings.enableExtraCssForVscodeInfoview + val extraCssForVscodeInfoviewChanged = + extraCssForVscodeInfoview.text != lean4Settings.extraCssForVscodeInfoview + val hoveringTimeBeforePopupNativeInfoviewDocChanged = + hoveringTimeBeforePopupNativeInfoviewDoc.number != lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc + val nativeInfoviewPopupTextWidth1Changed = + nativeInfoviewPopupMinWidthTextLengthUpperBound.number != lean4Settings.nativeInfoviewPopupMinWidthTextLengthUpperBound + val nativeInfoviewPopupTextWidth2Changed = + nativeInfoviewPopupMaxWidthTextLengthLowerBound.number != lean4Settings.nativeInfoviewPopupMaxWidthTextLengthLowerBound + val nativeInfoviewPopupPreferredMinWidthChanged = + nativeInfoviewPopupPreferredMinWidth.number != lean4Settings.nativeInfoviewPopupPreferredMinWidth + val nativeInfoviewPopupPreferredMaxWidthChanged = + nativeInfoviewPopupPreferredMaxWidth.number != lean4Settings.nativeInfoviewPopupPreferredMaxWidth + val enableLspCompletionChanged = enableLspCompletion.isSelected != lean4Settings.enableLspCompletion + return enableNativeInfoviewChanged || enableVscodeInfoviewChanged || enableExtraCssForVscodeInfoviewChanged || + extraCssForVscodeInfoviewChanged || hoveringTimeBeforePopupNativeInfoviewDocChanged || enableLspCompletionChanged || + nativeInfoviewPopupTextWidth1Changed || nativeInfoviewPopupTextWidth2Changed || + nativeInfoviewPopupPreferredMinWidthChanged || nativeInfoviewPopupPreferredMaxWidthChanged + } fun apply() { lean4Settings.enableNativeInfoview = enableNativeInfoview.isSelected @@ -168,16 +217,22 @@ class Lean4SettingsView { lean4Settings.enableExtraCssForVscodeInfoview = enableExtraCssForVscodeInfoview.isSelected lean4Settings.extraCssForVscodeInfoview = extraCssForVscodeInfoview.text lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc = hoveringTimeBeforePopupNativeInfoviewDoc.number + lean4Settings.nativeInfoviewPopupMinWidthTextLengthUpperBound = nativeInfoviewPopupMinWidthTextLengthUpperBound.number + lean4Settings.nativeInfoviewPopupMaxWidthTextLengthLowerBound = nativeInfoviewPopupMaxWidthTextLengthLowerBound.number + lean4Settings.nativeInfoviewPopupPreferredMinWidth = nativeInfoviewPopupPreferredMinWidth.number + lean4Settings.nativeInfoviewPopupPreferredMaxWidth = nativeInfoviewPopupPreferredMaxWidth.number lean4Settings.enableLspCompletion = enableLspCompletion.isSelected // TODO is it OK here runBlocking? // TODO full state runBlocking { - _events.emit(Lean4SettingsState( - lean4Settings.enableNativeInfoview, - lean4Settings.enableVscodeInfoview, - lean4Settings.enableExtraCssForVscodeInfoview, - lean4Settings.extraCssForVscodeInfoview, - )) + _events.emit( + Lean4SettingsState( + lean4Settings.enableNativeInfoview, + lean4Settings.enableVscodeInfoview, + lean4Settings.enableExtraCssForVscodeInfoview, + lean4Settings.extraCssForVscodeInfoview, + ) + ) } } @@ -187,6 +242,10 @@ class Lean4SettingsView { enableExtraCssForVscodeInfoview.isSelected = lean4Settings.enableExtraCssForVscodeInfoview extraCssForVscodeInfoview.text = lean4Settings.extraCssForVscodeInfoview hoveringTimeBeforePopupNativeInfoviewDoc.number = lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc + nativeInfoviewPopupMinWidthTextLengthUpperBound.number = lean4Settings.nativeInfoviewPopupMinWidthTextLengthUpperBound + nativeInfoviewPopupMaxWidthTextLengthLowerBound.number = lean4Settings.nativeInfoviewPopupMaxWidthTextLengthLowerBound + nativeInfoviewPopupPreferredMinWidth.number = lean4Settings.nativeInfoviewPopupPreferredMinWidth + nativeInfoviewPopupPreferredMaxWidth.number = lean4Settings.nativeInfoviewPopupPreferredMaxWidth enableLspCompletion.isSelected = lean4Settings.enableLspCompletion } @@ -196,9 +255,28 @@ class Lean4SettingsView { } group("Infoview Settings") { row { cell(enableNativeInfoview) } - labeled("Time limit for popping up native infoview doc (millis): ", hoveringTimeBeforePopupNativeInfoviewDoc).enabledIf(enableNativeInfoview.selected) + labeled( + "Time limit for popping up native infoview doc (millis): ", + hoveringTimeBeforePopupNativeInfoviewDoc + ).enabledIf(enableNativeInfoview.selected) + labeled( + "text length upper bound for using min width", + nativeInfoviewPopupMinWidthTextLengthUpperBound + ).enabledIf(enableNativeInfoview.selected) + labeled( + "text length lower bound for using max width", + nativeInfoviewPopupMaxWidthTextLengthLowerBound + ).enabledIf(enableNativeInfoview.selected) + labeled( + "native infoview min width", + nativeInfoviewPopupPreferredMinWidth + ).enabledIf(enableNativeInfoview.selected) + labeled( + "native infoview max width", + nativeInfoviewPopupPreferredMaxWidth + ).enabledIf(enableNativeInfoview.selected) row { cell(enableVscodeInfoview) } - row { cell(enableExtraCssForVscodeInfoview)} + row { cell(enableExtraCssForVscodeInfoview) } row { scrollCell(extraCssForVscodeInfoview).align(AlignX.FILL) } @@ -207,6 +285,7 @@ class Lean4SettingsView { companion object { private val _events = MutableSharedFlow() + // TODO maybe the state also indicates the change detail val events: SharedFlow = _events.asSharedFlow() } @@ -241,13 +320,20 @@ class Lean4Configurable : SearchableConfigurable { */ class BrowserInfoviewColorAndFontPanelFactory : ColorAndFontPanelFactory { override fun createPanel(options: ColorAndFontOptions): NewColorAndFontPanel { - val previewPanel: FontEditorPreview = object : FontEditorPreview(Supplier {options.selectedScheme }, true) { + val previewPanel: FontEditorPreview = object : FontEditorPreview(Supplier { options.selectedScheme }, true) { // override fun updateOptionsScheme(selectedScheme: EditorColorsScheme): EditorColorsScheme { // println("TODO") // return selectedScheme // } } - return object : NewColorAndFontPanel(SchemesPanel(options), BrowserInfoviewFontOptions(options), previewPanel, "BrowserInfoviewColorAndFontPanelFactoryTODO", null, null) { + return object : NewColorAndFontPanel( + SchemesPanel(options), + BrowserInfoviewFontOptions(options), + previewPanel, + "BrowserInfoviewColorAndFontPanelFactoryTODO", + null, + null + ) { override fun containsFontOptions(): Boolean { return true } diff --git a/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt b/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt index 753ac489..7f497ee2 100644 --- a/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt +++ b/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt @@ -15,9 +15,11 @@ 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.ui.scale.JBUIScale.scale import kotlinx.coroutines.CoroutineScope import kotlinx.coroutines.Dispatchers import kotlinx.coroutines.launch +import lean4ij.Lean4Settings import lean4ij.lsp.data.ContextInfo import lean4ij.lsp.data.InfoviewRender import lean4ij.lsp.data.InteractiveInfoParams @@ -28,8 +30,8 @@ import org.eclipse.lsp4j.TextDocumentIdentifier import java.awt.Dimension import javax.swing.JEditorPane import javax.swing.JPanel +import javax.swing.JTextPane 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 @@ -37,7 +39,9 @@ import kotlin.math.min * 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() { +class InfoviewPopupEditorPane(text: String, maxWidth: Int, maxHeight: Int) : JTextPane() { + + private val lean4Settings = service() init { val scheme = EditorColorsManager.getInstance().globalScheme @@ -48,22 +52,46 @@ class InfoviewPopupEditorPane(text: String, maxWidth: Int, maxHeight: Int) : JEd // TODO maybe some setting for this, font/size etc font = schemeFont this.text = text + val width = getPreferredContentWidth(text.length, preferredSize) + val height = getPreferredHeightByWidth(width) + preferredSize = Dimension(width, height) + } - // 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))) + /** + * code copied from [com.intellij.codeInsight.documentation.DocumentationEditorPane.getPreferredContentWidth] + */ + private fun getPreferredContentWidth(textLength: Int, preferredSize: Dimension): Int { + // Heuristics to calculate popup width based on the amount of the content. + // The proportions are set for 4 chars/1px in range between 200 and 1000 chars. + // 200 chars and less is 300px, 1000 chars and more is 500px. + // These values were calculated based on experiments with varied content and manual resizing to comfortable width. + val width1 = lean4Settings.nativeInfoviewPopupMinWidthTextLengthUpperBound + val width2 = lean4Settings.nativeInfoviewPopupMaxWidthTextLengthLowerBound + val minWidth = lean4Settings.nativeInfoviewPopupPreferredMinWidth + val maxWidth = lean4Settings.nativeInfoviewPopupPreferredMaxWidth + val contentLengthPreferredSize = if (textLength < width1) { + minWidth + } else if (textLength in (width1 + 1) until width2) { + minWidth + (textLength - width1) * (maxWidth - minWidth) / (width2 - width1) } else { - preferredSize = Dimension(result.width, result.height) + maxWidth } + return scale(contentLengthPreferredSize) + } + private var myCachedPreferredSize: Dimension? = null + + /** + * code copied from [com.intellij.codeInsight.documentation.DocumentationEditorPane.getPreferredHeightByWidth] + */ + private fun getPreferredHeightByWidth(width: Int): Int { + if (myCachedPreferredSize != null && myCachedPreferredSize!!.width == width) { + return myCachedPreferredSize!!.height + } + setSize(width, Short.MAX_VALUE.toInt()) + val result = preferredSize + myCachedPreferredSize = Dimension(width, result.height) + return myCachedPreferredSize!!.height } } @@ -85,10 +113,11 @@ class CodeWithInfosDocumentationHyperLink( */ private var height: Int? = null } + private var popupPanel: JBPopup? = null override fun navigate(project: Project) { - val leanProjectService : LeanProjectService = project.service() + val leanProjectService: LeanProjectService = project.service() leanProjectService.scope.launch { val session = leanProjectService.file(file).getSession() // file.url has format file://I:/.. whereas file.path has format "I:/..." in windows @@ -104,7 +133,10 @@ class CodeWithInfosDocumentationHyperLink( ) val infoToInteractive = leanProjectService.languageServer.await() .infoToInteractive(rpcParams) - var htmlDoc : String? = null + val sb = InfoviewRender() + val typeStr = infoToInteractive.type?.toInfoViewString(sb, null) ?: "" + val exprStr = infoToInteractive.exprExplicit?.toInfoViewString(sb, null) ?: "" + var htmlDoc: String? = null if (infoToInteractive.doc != null) { val markdownDoc: String = infoToInteractive.doc // val flavour = CommonMarkFlavourDescriptor() @@ -124,20 +156,23 @@ class CodeWithInfosDocumentationHyperLink( htmlDoc = htmlDoc.substring("

".length) } // TODO maybe some css for this? - htmlDoc = "${htmlDoc}" + val toolWindowSize = toolWindow.toolWindow.component.size + // htmlDoc = "${htmlDoc}" } - val sb = InfoviewRender() - val typeStr = infoToInteractive.type?.toInfoViewString(sb, null) ?: "" - val exprStr = infoToInteractive.exprExplicit?.toInfoViewString(sb, null) ?: "" // ref: https://plugins.jetbrains.com/docs/intellij/coroutine-tips-and-tricks.html // TODO here must limit the range in EDT + val doc = if (htmlDoc == null) { + "$exprStr : $typeStr" + } else { + "$exprStr : $typeStr

${htmlDoc}" + } launch(Dispatchers.EDT) { - createPopupPanel("$exprStr : $typeStr", htmlDoc) + createPopupPanel(doc) } } } - fun createDocPanel(doc: String): JEditorPane { + fun createDocPanel(doc: String, i: Int): JEditorPane { val toolWindowSize = toolWindow.toolWindow.component.size val maxWidth = toolWindowSize.width * 8 / 10 val maxHeight = toolWindowSize.height * 8 / 10 @@ -158,18 +193,18 @@ class CodeWithInfosDocumentationHyperLink( return exprPane } - fun createPopupPanel(typeAndExpr: String, doc: String?) { + /** + * TODO check [com.intellij.codeInsight.documentation.DocumentationScrollPane.setViewportView] + */ + fun createPopupPanel(doc: String) { val factory = JBPopupFactory.getInstance() - val typeAndExprPanel = createExprPanel(typeAndExpr) + val toolWindowSize = toolWindow.toolWindow.component.size + val docPanel = createDocPanel(doc, toolWindowSize.width * 8 / 10) val jPanel = JPanel(VerticalLayout(1)) - jPanel.add(typeAndExprPanel) - if (doc != null) { - val docPanel = createDocPanel(doc) - jPanel.add(docPanel) - } + jPanel.add(docPanel) val popup = JBScrollPane(jPanel) popup.verticalScrollBarPolicy = ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED - popup.horizontalScrollBarPolicy = ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER + popup.horizontalScrollBarPolicy = ScrollPaneConstants.HORIZONTAL_SCROLLBAR_AS_NEEDED popupPanel = factory.createComponentPopupBuilder(popup, popup) // .setTitle(title) @@ -177,11 +212,11 @@ class CodeWithInfosDocumentationHyperLink( .setMovable(true) .setRequestFocus(true) .createPopup() - // .showInScreenCoordinates(toolWindow.toolWindow.component, point) - // .showInBestPositionFor(editor) - // .showInCenterOf(toolWindow.component) - // .showInFocusCenter() - // .show(factory.guessBestPopupLocation(toolWindow.toolWindow.component)) + // .showInScreenCoordinates(toolWindow.toolWindow.component, point) + // .showInBestPositionFor(editor) + // .showInCenterOf(toolWindow.component) + // .showInFocusCenter() + // .show(factory.guessBestPopupLocation(toolWindow.toolWindow.component)) popupPanel?.show(point) } From f925504d836ec248f152f6b1f6ed488d30286e5b Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Sun, 13 Oct 2024 14:57:09 +0800 Subject: [PATCH 06/11] remove click in internal infoview, some optimization for popup up doc --- CHANGELOG.md | 3 + .../infoview/InfoviewMouseMotionListener.kt | 103 +++++++++++------- ...rLink.kt => InfoviewPopupDocumentation.kt} | 2 +- .../lean4ij/infoview/LeanInfoViewWindow.kt | 9 +- 4 files changed, 72 insertions(+), 45 deletions(-) rename src/main/kotlin/lean4ij/infoview/{CodeWithInfosDocumentationHyperLink.kt => InfoviewPopupDocumentation.kt} (99%) diff --git a/CHANGELOG.md b/CHANGELOG.md index 510cae8c..bab63a6c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,9 @@ ## [Unreleased] - fix caret of internal infoview at first line first col while refreshing +- tuning size for internal infoview popup window +- remove click in internal infoview, some optimization for popup up doc + ## [0.0.17] - 2024-10-06 Depend on the latest approved nightly build of LSP4IJ: 0.7.0-20241006-013203 diff --git a/src/main/kotlin/lean4ij/infoview/InfoviewMouseMotionListener.kt b/src/main/kotlin/lean4ij/infoview/InfoviewMouseMotionListener.kt index d7cb3b5d..81c739a8 100644 --- a/src/main/kotlin/lean4ij/infoview/InfoviewMouseMotionListener.kt +++ b/src/main/kotlin/lean4ij/infoview/InfoviewMouseMotionListener.kt @@ -3,10 +3,14 @@ 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 import com.intellij.openapi.editor.event.EditorMouseEvent import com.intellij.openapi.editor.event.EditorMouseMotionListener +import com.intellij.openapi.editor.ex.EditorEx +import com.intellij.openapi.editor.markup.HighlighterLayer +import com.intellij.openapi.editor.markup.HighlighterTargetArea import com.intellij.openapi.editor.markup.RangeHighlighter import com.intellij.openapi.editor.markup.TextAttributes import com.intellij.openapi.vfs.VirtualFile @@ -16,7 +20,10 @@ import kotlinx.coroutines.channels.Channel import kotlinx.coroutines.launch import kotlinx.coroutines.withTimeout import lean4ij.Lean4Settings -import lean4ij.lsp.data.* +import lean4ij.lsp.data.ContextInfo +import lean4ij.lsp.data.InteractiveDiagnostics +import lean4ij.lsp.data.InteractiveGoals +import lean4ij.lsp.data.InteractiveTermGoal import lean4ij.project.LeanProjectService import java.awt.Color @@ -26,7 +33,7 @@ import java.awt.Color class InfoviewMouseMotionListener( private val leanProjectService: LeanProjectService, private val infoViewWindow: LeanInfoViewWindow, - private val support: EditorHyperlinkSupport, + private val editor: EditorEx, private val file: VirtualFile, private val logicalPosition: LogicalPosition, private val interactiveGoals: InteractiveGoals?, @@ -36,15 +43,18 @@ class InfoviewMouseMotionListener( ) : EditorMouseMotionListener { private val lean4Settings = service() private var hyperLink: RangeHighlighter? = null + private val support = EditorHyperlinkSupport.get(editor) override fun mouseMoved(e: EditorMouseEvent) { - emitOffset(e.offset) if (hyperLink != null) { support.removeHyperlink(hyperLink!!) } if (!e.isOverText) { + leanProjectService.scope.launch { + offsetsFlow.send(null) + } return } - var c : Triple? = null + var c: Triple? = null if (interactiveGoals != null) { c = interactiveGoals.getCodeText(e.offset) } @@ -69,35 +79,51 @@ class InfoviewMouseMotionListener( } } if (c == null) { + leanProjectService.scope.launch { + offsetsFlow.send(null) + } return } - hyperLink = support.createHyperlink( - c.second, - c.third, - object : TextAttributes() { - override fun getBackgroundColor(): Color { - // TODO document this - // TODO should scheme be cache? - val scheme = EditorColorsManager.getInstance().globalScheme - // TODO customize attr? or would backgroundColor null? - // indeed here it can be null, don't know why Kotlin does not mark it as error - return scheme.getAttributes(EditorColors.IDENTIFIER_UNDER_CARET_ATTRIBUTES).backgroundColor - } - }, - CodeWithInfosDocumentationHyperLink(leanProjectService.scope, infoViewWindow, file, logicalPosition, c.first, - RelativePoint(e.mouseEvent) ) - ) + val attr = object : TextAttributes() { + override fun getBackgroundColor(): Color { + // TODO document this + // TODO should scheme be cache? + val scheme = EditorColorsManager.getInstance().globalScheme + // TODO customize attr? or would backgroundColor null? + // indeed here it can be null, don't know why Kotlin does not mark it as error + return scheme.getAttributes(EditorColors.IDENTIFIER_UNDER_CARET_ATTRIBUTES).backgroundColor + } + } + createPopup(c, attr) + leanProjectService.scope.launch { + offsetsFlow.send( + InfoviewPopupDocumentation( + leanProjectService.scope, infoViewWindow, file, logicalPosition, c.first, + RelativePoint(e.mouseEvent) + ) + ) + } } - private var offsetsFlow = Channel() - - private fun emitOffset(offset: Int) { - leanProjectService.scope.launch { - offsetsFlow.send(offset) + /** + * this is some kind copy from [com.intellij.execution.impl.EditorHyperlinkSupport.createHyperlink] + */ + private fun createPopup(c: Triple, attr: TextAttributes) { + hyperLink = editor.markupModel.addRangeHighlighterAndChangeAttributes( + CodeInsightColors.HYPERLINK_ATTRIBUTES, + c.second, + c.third, + HighlighterLayer.HYPERLINK, + HighlighterTargetArea.EXACT_RANGE, + false + ) { ex -> + ex.textAttributes = attr } } + private var offsetsFlow = Channel() + init { leanProjectService.scope.launch { tryEmitHover() @@ -105,32 +131,27 @@ class InfoviewMouseMotionListener( } private suspend fun tryEmitHover() { - var oldHovering: CodeWithInfosDocumentationHyperLink? = null - var isHovering = false - var oldOffset = -1 - var offset = -1 + var oldHovering: InfoviewPopupDocumentation? = null + var hovering: InfoviewPopupDocumentation? = null // TODO is it OK here using infinite loop? // should it be some disposal behavior? while (true) { try { // TODO the time control here seems problematic // it seems longer than the setting - offset = withTimeout(lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc.toLong()) { + hovering = withTimeout(lean4Settings.hoveringTimeBeforePopupNativeInfoviewDoc.toLong()) { offsetsFlow.receive() } - isHovering = false - oldHovering?.cancel() + if (oldHovering != null && oldHovering.contextInfo != hovering?.contextInfo) { + oldHovering.cancel() + oldHovering = null + } } catch (e: TimeoutCancellationException) { - if (offset == oldOffset && oldOffset != -1 && !isHovering) { - isHovering = true - val hyperLink = support.getHyperlinkAt(offset) - if (hyperLink != null) { - oldHovering?.cancel() - oldHovering = hyperLink as CodeWithInfosDocumentationHyperLink - oldHovering.navigate(leanProjectService.project) - } + if (hovering != null && hovering != oldHovering && hovering.contextInfo != oldHovering?.contextInfo) { + oldHovering?.cancel() + oldHovering = hovering + hovering.navigate(leanProjectService.project) } - oldOffset = offset } } } diff --git a/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt b/src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt similarity index 99% rename from src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt rename to src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt index 7f497ee2..d6aff247 100644 --- a/src/main/kotlin/lean4ij/infoview/CodeWithInfosDocumentationHyperLink.kt +++ b/src/main/kotlin/lean4ij/infoview/InfoviewPopupDocumentation.kt @@ -98,7 +98,7 @@ class InfoviewPopupEditorPane(text: String, maxWidth: Int, maxHeight: Int) : JTe /** * TODO this class absolutely need some refactor and a better implementation */ -class CodeWithInfosDocumentationHyperLink( +class InfoviewPopupDocumentation( val scope: CoroutineScope, val toolWindow: LeanInfoViewWindow, val file: VirtualFile, diff --git a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt index da638b88..51293c34 100644 --- a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt +++ b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindow.kt @@ -1,13 +1,12 @@ package lean4ij.infoview -import com.intellij.codeInsight.codeVision.ui.mousePoint import com.intellij.execution.impl.EditorHyperlinkSupport 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.event.EditorMouseListener +import com.intellij.openapi.editor.ScrollType import com.intellij.openapi.editor.event.EditorMouseMotionListener import com.intellij.openapi.editor.ex.EditorEx import com.intellij.openapi.editor.ex.FoldingListener @@ -144,9 +143,13 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru val editorEx: EditorEx = editor.await() editorEx.markupModel.removeAllHighlighters() editorEx.document.setText(interactiveInfo.toString()) + + // TODO maybe a configuration for this // 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.scrollingModel.scrollToCaret(ScrollType.CENTER) + editorEx.foldingModel.runBatchFoldingOperation { editorEx.foldingModel.clearFoldRegions() var allMessagesFoldRegion : FoldRegion? = null @@ -182,7 +185,7 @@ class LeanInfoViewWindow(val toolWindow: ToolWindow) : SimpleToolWindowPanel(tru if (mouseMotionListener != null) { editorEx.removeEditorMouseMotionListener(mouseMotionListener!!) } - mouseMotionListener = InfoviewMouseMotionListener(leanProject, this, support, file, logicalPosition, + mouseMotionListener = InfoviewMouseMotionListener(leanProject, this, editorEx, file, logicalPosition, interactiveGoals, interactiveTermGoal, interactiveDiagnostics, interactiveDiagnosticsAllMessages) editorEx.addEditorMouseMotionListener(mouseMotionListener!!) } From af5fe662671d980d00b238d5e1f11285affa3b71 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Sun, 13 Oct 2024 19:37:24 +0800 Subject: [PATCH 07/11] add setting for disable lsp completion --- .../lean4ij/lsp/LeanLSPCompletionFeature.kt | 18 ++++++++++++++++++ .../lean4ij/lsp/LeanLanguageServerFactory.kt | 10 ++++++++-- 2 files changed, 26 insertions(+), 2 deletions(-) create mode 100644 src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt diff --git a/src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt b/src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt new file mode 100644 index 00000000..40e9c98c --- /dev/null +++ b/src/main/kotlin/lean4ij/lsp/LeanLSPCompletionFeature.kt @@ -0,0 +1,18 @@ +package lean4ij.lsp + +import com.intellij.openapi.components.service +import com.intellij.psi.PsiFile +import com.redhat.devtools.lsp4ij.client.features.LSPCompletionFeature +import lean4ij.Lean4Settings + +/** + * Add an impl for disable lsp completion for lean + * for sometimes it's slow... + */ +class LeanLSPCompletionFeature : LSPCompletionFeature() { + private val lean4Settings = service() + + override fun isEnabled(file: PsiFile): Boolean { + return lean4Settings.enableLspCompletion + } +} \ No newline at end of file diff --git a/src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt b/src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt index d2f8c155..1bda9d7e 100644 --- a/src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt +++ b/src/main/kotlin/lean4ij/lsp/LeanLanguageServerFactory.kt @@ -5,7 +5,6 @@ import com.redhat.devtools.lsp4ij.LanguageServerEnablementSupport import com.redhat.devtools.lsp4ij.LanguageServerFactory import com.redhat.devtools.lsp4ij.client.LanguageClientImpl import com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures -import com.redhat.devtools.lsp4ij.client.features.LSPCompletionFeature import com.redhat.devtools.lsp4ij.server.StreamConnectionProvider import org.eclipse.lsp4j.services.LanguageServer import java.util.concurrent.atomic.AtomicBoolean @@ -51,4 +50,11 @@ class LeanLanguageServerFactory : LanguageServerFactory, LanguageServerEnablemen override fun getServerInterface(): Class { return InternalLeanLanguageServer::class.java } -} \ No newline at end of file + + override fun createClientFeatures(): LSPClientFeatures { + return LSPClientFeatures().apply { + completionFeature = LeanLSPCompletionFeature() + } + } +} + From 0e2401dc1136797abd182641e79ea46fedb2ebb0 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Sun, 13 Oct 2024 22:41:43 +0800 Subject: [PATCH 08/11] add a config for the comment prefix for goal hint --- src/main/kotlin/lean4ij/Lean4Configurable.kt | 22 +++++++++++++++++++ .../InfoviewInlayHintsProviderFactory.kt | 5 +++-- .../kotlin/lean4ij/lsp/data/SubexprInfo.kt | 3 +++ 3 files changed, 28 insertions(+), 2 deletions(-) diff --git a/src/main/kotlin/lean4ij/Lean4Configurable.kt b/src/main/kotlin/lean4ij/Lean4Configurable.kt index b7c2e878..c21de940 100644 --- a/src/main/kotlin/lean4ij/Lean4Configurable.kt +++ b/src/main/kotlin/lean4ij/Lean4Configurable.kt @@ -17,6 +17,7 @@ import com.intellij.openapi.options.SearchableConfigurable import com.intellij.ui.JBIntSpinner import com.intellij.ui.components.JBCheckBox import com.intellij.ui.components.JBTextArea +import com.intellij.ui.components.JBTextField import com.intellij.ui.dsl.builder.AlignX import com.intellij.ui.dsl.builder.COLUMNS_SHORT import com.intellij.ui.dsl.builder.Cell @@ -31,6 +32,7 @@ import kotlinx.coroutines.flow.SharedFlow import kotlinx.coroutines.flow.asSharedFlow import kotlinx.coroutines.runBlocking import lean4ij.infoview.external.createThemeCss +import org.ini4j.Reg import java.awt.Component import java.util.function.Supplier import javax.swing.AbstractButton @@ -78,6 +80,8 @@ class ToolTipListCellRenderer(private val toolTips: List) : DefaultListC // extra class class Lean4Settings : PersistentStateComponent { + var commentPrefixForGoalHint : String = "-- :" + var commentPrefixForGoalHintRegex = Regex("""(\n\s*${commentPrefixForGoalHint})\s*?\n\s*\S""") var enableLspCompletion = true var enableNativeInfoview = true @@ -101,6 +105,7 @@ class Lean4Settings : PersistentStateComponent { override fun loadState(state: Lean4Settings) { XmlSerializerUtil.copyBean(state, this) + commentPrefixForGoalHintRegex = Regex("""(\n\s*${commentPrefixForGoalHint})\s*?\n\s*\S""") } } @@ -119,6 +124,8 @@ data class Lean4SettingsState( */ class Lean4SettingsView { private val lean4Settings = service() + + private val commentPrefixForGoalHint = JBTextField(lean4Settings.commentPrefixForGoalHint) private val enableLspCompletion = JBCheckBox("Enable lsp completion", lean4Settings.enableLspCompletion) @@ -186,8 +193,15 @@ class Lean4SettingsView { } } + /** + * TODO one setting, 5 positions must be changed... [Lean4Settings], [Lean4SettingsView], here [isModified], [apply], [reset], + * there must be some more clean way with declaration style + */ val isModified: Boolean get() { + + val commentPrefixForGoalHintChanged = commentPrefixForGoalHint.text != lean4Settings.commentPrefixForGoalHint + val enableNativeInfoviewChanged = enableNativeInfoview.isSelected != lean4Settings.enableNativeInfoview val enableVscodeInfoviewChanged = enableVscodeInfoview.isSelected != lean4Settings.enableVscodeInfoview val enableExtraCssForVscodeInfoviewChanged = @@ -209,9 +223,13 @@ class Lean4SettingsView { extraCssForVscodeInfoviewChanged || hoveringTimeBeforePopupNativeInfoviewDocChanged || enableLspCompletionChanged || nativeInfoviewPopupTextWidth1Changed || nativeInfoviewPopupTextWidth2Changed || nativeInfoviewPopupPreferredMinWidthChanged || nativeInfoviewPopupPreferredMaxWidthChanged + || commentPrefixForGoalHintChanged } fun apply() { + lean4Settings.commentPrefixForGoalHint = commentPrefixForGoalHint.text + lean4Settings.commentPrefixForGoalHintRegex = Regex("""(\n\s*${lean4Settings.commentPrefixForGoalHint})\s*?\n\s*\S""") + lean4Settings.enableNativeInfoview = enableNativeInfoview.isSelected lean4Settings.enableVscodeInfoview = enableVscodeInfoview.isSelected lean4Settings.enableExtraCssForVscodeInfoview = enableExtraCssForVscodeInfoview.isSelected @@ -237,6 +255,7 @@ class Lean4SettingsView { } fun reset() { + commentPrefixForGoalHint.text = lean4Settings.commentPrefixForGoalHint enableNativeInfoview.isSelected = lean4Settings.enableNativeInfoview enableVscodeInfoview.isSelected = lean4Settings.enableVscodeInfoview enableExtraCssForVscodeInfoview.isSelected = lean4Settings.enableExtraCssForVscodeInfoview @@ -250,6 +269,9 @@ class Lean4SettingsView { } fun createComponent() = panel { + group("Inlay Hints Settings ") { + labeled("Comment prefix for goal hints", commentPrefixForGoalHint) + } group("Language Server Settings") { row { cell(enableLspCompletion) } } diff --git a/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt b/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt index 54b43b0b..2cebbff9 100644 --- a/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt +++ b/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt @@ -22,6 +22,7 @@ import com.intellij.psi.PsiElement import com.intellij.psi.PsiFile import com.intellij.util.io.await import kotlinx.coroutines.launch +import lean4ij.Lean4Settings import lean4ij.lsp.data.InfoviewRender import lean4ij.lsp.data.InteractiveGoalsParams import lean4ij.lsp.data.InteractiveTermGoalParams @@ -238,13 +239,13 @@ class OmitTypeInlayHintsProvider : InlayHintsProvider { class GoalInlayHintsCollector(editor: Editor, project: Project?) : InlayHintBase(editor, project) { companion object { - val GOAL_REGEX = Regex("""(\n\s*-- :)\s*?\n\s*\S""") + val lean4Settings = service() } override suspend fun computeFor(file: LeanFile, content: String): HintSet { val hints = HintSet() - for (m in GOAL_REGEX.findAll(content)) { + for (m in lean4Settings.commentPrefixForGoalHintRegex.findAll(content)) { val session = file.getSession() val lineColumn = StringUtil.offsetToLineColumn(content, m.range.last) diff --git a/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt b/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt index 470ce4f5..c60caaae 100644 --- a/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt +++ b/src/main/kotlin/lean4ij/lsp/data/SubexprInfo.kt @@ -24,6 +24,9 @@ data class SubexprInfo (val subexprPos: String, val info: ContextInfo, val diffS "willChange" -> { sb.highlight(startOffset, endOffset, TextAttributesKeys.RemovedText) } + "willDelete" -> { + sb.highlight(startOffset, endOffset, TextAttributesKeys.RemovedText) + } else -> { // should not be here TODO("diffStatus: $diffStatus for infoview change not defined") From f6a91b245f0060cd41e41f39348fb07acb8cf261 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Sun, 13 Oct 2024 23:16:28 +0800 Subject: [PATCH 09/11] update workflow --- .github/workflows/build.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index f7f44d7b..f76fa4d7 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -16,7 +16,10 @@ name: Build on: # Trigger the workflow on pushes to only the 'main' branch (this avoids duplicate checks being run e.g., for dependabot pull requests) push: - branches: [ main ] + branches: + - main + # also on feat branches + - feat/.+ # Trigger the workflow on any pull request pull_request: From 1aa8cd187d34cd8381a2ab2ce932a0b03c728586 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Sun, 13 Oct 2024 23:34:52 +0800 Subject: [PATCH 10/11] revert worflow conf, use PR --- .github/workflows/build.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index f76fa4d7..cc3debd8 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -19,7 +19,8 @@ on: branches: - main # also on feat branches - - feat/.+ + # this does not work + # - feat/.+ # Trigger the workflow on any pull request pull_request: From 5962046f178e94170875a4b02f266ea283cf8316 Mon Sep 17 00:00:00 2001 From: Shanghe Chen Date: Mon, 14 Oct 2024 00:15:51 +0800 Subject: [PATCH 11/11] remove internal api --- src/main/kotlin/lean4ij/Lean4Configurable.kt | 41 -------------------- src/main/resources/META-INF/plugin.xml | 2 - 2 files changed, 43 deletions(-) diff --git a/src/main/kotlin/lean4ij/Lean4Configurable.kt b/src/main/kotlin/lean4ij/Lean4Configurable.kt index b7c2e878..fb9508b8 100644 --- a/src/main/kotlin/lean4ij/Lean4Configurable.kt +++ b/src/main/kotlin/lean4ij/Lean4Configurable.kt @@ -313,45 +313,4 @@ class Lean4Configurable : SearchableConfigurable { settingsView = Lean4SettingsView() return settingsView?.createComponent() } -} - -/** - * The class is mainly from [com.intellij.application.options.colors.ColorAndFontOptions.ConsoleFontConfigurableFactory] - */ -class BrowserInfoviewColorAndFontPanelFactory : ColorAndFontPanelFactory { - override fun createPanel(options: ColorAndFontOptions): NewColorAndFontPanel { - val previewPanel: FontEditorPreview = object : FontEditorPreview(Supplier { options.selectedScheme }, true) { - // override fun updateOptionsScheme(selectedScheme: EditorColorsScheme): EditorColorsScheme { - // println("TODO") - // return selectedScheme - // } - } - return object : NewColorAndFontPanel( - SchemesPanel(options), - BrowserInfoviewFontOptions(options), - previewPanel, - "BrowserInfoviewColorAndFontPanelFactoryTODO", - null, - null - ) { - override fun containsFontOptions(): Boolean { - return true - } - } - } - - override fun getPanelDisplayName(): String { - return "Lean4 Browser Infoview Font" - } -} - -/** - * This class is mainly from [com.intellij.application.options.colors.ConsoleFontOptions] - */ -class BrowserInfoviewFontOptions(options: ColorAndFontOptions) : FontOptions(options) { - - override fun getOverwriteFontTitle(): String { - return "Use Browser infoview font instead of the" - } - } \ No newline at end of file diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml index f1b47d9f..36ffbcd7 100644 --- a/src/main/resources/META-INF/plugin.xml +++ b/src/main/resources/META-INF/plugin.xml @@ -65,8 +65,6 @@ - -