Merge pull request #29 from onriv/feat/eol-hints

Feature: Diagnostic Hints
onriv · Oct 19, 2024 · 132d0d6 · 132d0d6
2 parents e89c513 + 772ed7e
commit 132d0d6
Show file tree

Hide file tree

Showing 9 changed files with 409 additions and 54 deletions.
diff --git a/src/main/kotlin/lean4ij/Lean4Configurable.kt b/src/main/kotlin/lean4ij/Lean4Configurable.kt
@@ -32,9 +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
 import javax.swing.DefaultListCellRenderer
 import javax.swing.JComponent
@@ -82,6 +80,7 @@ class Lean4Settings : PersistentStateComponent<Lean4Settings> {
 
     var commentPrefixForGoalHint : String = "---"
     var commentPrefixForGoalHintRegex = updateCommentPrefixForGoalHintRegex()
+    var enableDiagnosticsLens = true
     var enableLspCompletion = true
 
     var enableNativeInfoview = true
@@ -129,6 +128,7 @@ class Lean4SettingsView {
     private val lean4Settings = service<Lean4Settings>()
 
     private val commentPrefixForGoalHint = JBTextField(lean4Settings.commentPrefixForGoalHint)
+    private val enableDiagnosticLens = JBCheckBox("Enable diagnostics lens for #check, #print, etc", lean4Settings.enableLspCompletion)
 
     private val enableLspCompletion = JBCheckBox("Enable lsp completion", lean4Settings.enableLspCompletion)
 
@@ -222,16 +222,19 @@ class Lean4SettingsView {
             val nativeInfoviewPopupPreferredMaxWidthChanged =
                 nativeInfoviewPopupPreferredMaxWidth.number != lean4Settings.nativeInfoviewPopupPreferredMaxWidth
             val enableLspCompletionChanged = enableLspCompletion.isSelected != lean4Settings.enableLspCompletion
+            val enableDiagnosticLensChanged = enableDiagnosticLens.isSelected != lean4Settings.enableDiagnosticsLens
             return enableNativeInfoviewChanged || enableVscodeInfoviewChanged || enableExtraCssForVscodeInfoviewChanged ||
                     extraCssForVscodeInfoviewChanged || hoveringTimeBeforePopupNativeInfoviewDocChanged || enableLspCompletionChanged ||
                     nativeInfoviewPopupTextWidth1Changed || nativeInfoviewPopupTextWidth2Changed ||
                     nativeInfoviewPopupPreferredMinWidthChanged || nativeInfoviewPopupPreferredMaxWidthChanged
                     || commentPrefixForGoalHintChanged
+                    || enableDiagnosticLensChanged
         }
 
     fun apply() {
         lean4Settings.commentPrefixForGoalHint = commentPrefixForGoalHint.text
         lean4Settings.commentPrefixForGoalHintRegex = Regex("""(\n\s*${lean4Settings.commentPrefixForGoalHint})\s*?\n\s*\S""")
+        lean4Settings.enableDiagnosticsLens = enableDiagnosticLens.isSelected
 
         lean4Settings.enableNativeInfoview = enableNativeInfoview.isSelected
         lean4Settings.enableVscodeInfoview = enableVscodeInfoview.isSelected
@@ -258,6 +261,7 @@ class Lean4SettingsView {
     }
 
     fun reset() {
+        enableDiagnosticLens.isSelected = lean4Settings.enableDiagnosticsLens
         commentPrefixForGoalHint.text = lean4Settings.commentPrefixForGoalHint
         enableNativeInfoview.isSelected = lean4Settings.enableNativeInfoview
         enableVscodeInfoview.isSelected = lean4Settings.enableVscodeInfoview
@@ -273,6 +277,7 @@ class Lean4SettingsView {
 
     fun createComponent() = panel {
         group("Inlay Hints Settings ") {
+            row { cell(enableDiagnosticLens) }
             labeled("Comment prefix for goal hints", commentPrefixForGoalHint)
         }
         group("Language Server Settings") {

diff --git a/src/main/kotlin/lean4ij/actions/AddInlayGoalHint.kt b/src/main/kotlin/lean4ij/actions/AddInlayGoalHint.kt
@@ -0,0 +1,95 @@
+package lean4ij.actions
+
+import com.intellij.openapi.actionSystem.ActionUpdateThread
+import com.intellij.openapi.actionSystem.AnAction
+import com.intellij.openapi.actionSystem.AnActionEvent
+import com.intellij.openapi.actionSystem.CommonDataKeys
+import com.intellij.openapi.application.WriteAction
+import com.intellij.openapi.command.CommandProcessor
+import com.intellij.openapi.components.service
+import com.intellij.openapi.editor.Editor
+import com.intellij.openapi.util.text.StringUtil
+import lean4ij.Lean4Settings
+
+class AddInlayGoalHint : AnAction() {
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT
+    }
+
+    override fun update(e: AnActionEvent) {
+        e.presentation.setEnabledAndVisible(e.getData(CommonDataKeys.EDITOR) != null);
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        val editor: Editor = e.getRequiredData(CommonDataKeys.EDITOR);
+        val selector = editor.selectionModel
+        val selectionStart = selector.selectionStart
+
+        val settings = service<Lean4Settings>();
+
+        val lineCol = StringUtil.offsetToLineColumn(editor.document.text, selectionStart);
+        val at = selectionStart - lineCol.column;
+        val text = editor.document.text
+        var endIndex = at
+        while (endIndex < text.length && text[endIndex].isWhitespace() && text[endIndex] != '\n') {
+            endIndex++
+        }
+        val whitespacePrefix = text.subSequence(at, endIndex)
+
+        // only perform action if not already present in previous line
+        if (lineCol.line != 0) {
+            val prevStart = StringUtil.lineColToOffset(text, lineCol.line - 1, 0);
+            val prev = text.substring(prevStart, at).trim();
+            if (prev == settings.commentPrefixForGoalHint) {
+                return;
+            }
+        }
+
+        WriteAction.run<Throwable> {
+            CommandProcessor.getInstance().executeCommand(e.project, {
+                editor.document.insertString(at, "${whitespacePrefix}${settings.commentPrefixForGoalHint}\n")
+            }, "Insert Goal Hint", "lean4ij.insertGoalHintCommand");
+        }
+    }
+}
+class DelInlayGoalHint : AnAction() {
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT
+    }
+
+    override fun update(e: AnActionEvent) {
+        e.presentation.setEnabledAndVisible(e.getData(CommonDataKeys.EDITOR) != null);
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        val editor: Editor = e.getRequiredData(CommonDataKeys.EDITOR);
+        val selector = editor.selectionModel
+        val selectionStart = selector.selectionStart
+        val selectionEnd = selector.selectionEnd
+
+        val settings = service<Lean4Settings>();
+
+        val lastLine = StringUtil.offsetToLineColumn(editor.document.text, selectionEnd).line;
+        var firstLine = StringUtil.offsetToLineColumn(editor.document.text, selectionStart).line;
+        if (selectionStart == selectionEnd) {
+            firstLine = maxOf(0, firstLine - 1);
+        }
+
+        WriteAction.run<Throwable> {
+            for (i in lastLine downTo firstLine) {
+
+                val text = editor.document.text
+                val lineStart = StringUtil.lineColToOffset(text, i, 0);
+                val lineEnd = StringUtil.lineColToOffset(text, i + 1, 0);
+                val line = text.substring(lineStart, lineEnd).trim();
+                if (line == settings.commentPrefixForGoalHint) {
+                    CommandProcessor.getInstance().executeCommand(e.project, {
+                        editor.document.deleteString(lineStart, lineEnd)
+                    }, "Delete Goal Hint", "lean4ij.deleteGoalHintCommand");
+                }
+            }
+        }
+    }
+}