working on external infoview search, adding search text field

CHANGELOG.md

@@ -8,6 +8,8 @@
 - remove a dependent log in CHANGELOG.md in build.gradle.kts
 - add suffix triggering or debounce triggering strategies for "goto workspace symbols/classes" in settings
 - make "open in find tool window" of "goto workspace symbols/classes" work
+- goto definition for internal infoview
+- add search for external infoview
 
 ## [0.1.9] - 2024-12-16
 

src/main/kotlin/lean4ij/actions/FindInExternalInfoview.kt

@@ -0,0 +1,37 @@
+package lean4ij.actions
+
+import com.intellij.icons.AllIcons
+import com.intellij.openapi.actionSystem.ActionUpdateThread
+import com.intellij.openapi.actionSystem.AnAction
+import com.intellij.openapi.actionSystem.AnActionEvent
+import com.intellij.openapi.components.service
+import kotlinx.coroutines.launch
+import lean4ij.infoview.external.JcefInfoviewService
+import lean4ij.util.leanProjectScope
+
+class FindInExternalInfoview : AnAction() {
+
+    init {
+        templatePresentation.icon = AllIcons.Actions.Find
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        val project = e.project ?: return
+        val jcefInfoviewService = project.service<JcefInfoviewService>()
+        jcefInfoviewService.searchTextField.isVisible = !jcefInfoviewService.searchTextField.isVisible
+        if (!jcefInfoviewService.searchTextField.isVisible) {
+            project.leanProjectScope.launch {
+                jcefInfoviewService.searchTextFlow.send("")
+            }
+            return
+        }
+        project.leanProjectScope.launch {
+            jcefInfoviewService.searchTextFlow.send(jcefInfoviewService.searchTextField.text)
+        }
+
+    }
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT;
+    }
+}

src/main/kotlin/lean4ij/actions/RestartInternalInfoview.kt

@@ -0,0 +1,32 @@
+package lean4ij.actions
+
+import com.intellij.icons.AllIcons
+import com.intellij.openapi.actionSystem.ActionUpdateThread
+import com.intellij.openapi.actionSystem.AnAction
+import com.intellij.openapi.actionSystem.AnActionEvent
+import com.intellij.openapi.components.service
+import com.intellij.openapi.fileEditor.FileEditorManager
+import lean4ij.infoview.LeanInfoviewService
+import lean4ij.project.LeanProjectService
+
+class RestartInternalInfoview : AnAction() {
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT
+    }
+
+    init {
+        templatePresentation.icon = AllIcons.Actions.Restart
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        val project = e.project?:return
+        FileEditorManager.getInstance(project).selectedTextEditor?.let { editor ->
+            // TODO here in fact message up two things:
+            //      one is recreating a new editor for removing old editor's bug
+            //      the other is updating infoview manually
+            project.service<LeanInfoviewService>().toolWindow?.restartEditor()
+            project.service<LeanProjectService>().updateInfoviewFor(editor, true)
+        }
+    }
+}

src/main/kotlin/lean4ij/actions/RestartJcefInfoview.kt

@@ -5,12 +5,7 @@ import com.intellij.openapi.actionSystem.ActionUpdateThread
 import com.intellij.openapi.actionSystem.AnAction
 import com.intellij.openapi.actionSystem.AnActionEvent
 import com.intellij.openapi.components.service
-import com.intellij.openapi.fileEditor.FileEditorManager
-import com.intellij.openapi.util.IconLoader.getIcon
-import lean4ij.infoview.LeanInfoviewService
 import lean4ij.infoview.external.JcefInfoviewService
-import lean4ij.project.LeanProjectService
-import javax.swing.Icon
 
 class RestartJcefInfoview : AnAction() {
 
@@ -28,53 +23,3 @@ class RestartJcefInfoview : AnAction() {
 
 }
 
-class RestartInternalInfoview : AnAction() {
-
-    override fun getActionUpdateThread(): ActionUpdateThread {
-        return ActionUpdateThread.BGT
-    }
-
-    init {
-        templatePresentation.icon = AllIcons.Actions.Restart
-    }
-
-    override fun actionPerformed(e: AnActionEvent) {
-        val project = e.project?:return
-        FileEditorManager.getInstance(project).selectedTextEditor?.let { editor ->
-            // TODO here in fact message up two things:
-            //      one is recreating a new editor for removing old editor's bug
-            //      the other is updating infoview manually
-            project.service<LeanInfoviewService>().toolWindow?.restartEditor()
-            project.service<LeanProjectService>().updateInfoviewFor(editor, true)
-        }
-    }
-}
-
-/**
- * TODO maybe add some buttons/actions for stop/start/toggle automatically refreshing the infoview
- *      which turn it into a manual mode
- */
-class ToggleAutomaticallyRefreshInternalInfoview : AnAction() {
-
-    private val onIcon: Icon = getIcon("/icons/textAutoGenerate.svg", javaClass)
-    private val offIcon: Icon = AllIcons.Actions.Suspend
-    init {
-        templatePresentation.icon = onIcon
-        templatePresentation.disabledIcon = offIcon
-    }
-
-    override fun actionPerformed(e: AnActionEvent) {
-        val project = e.project?:return
-        val leanInfoviewService = project.service<LeanInfoviewService>()
-        leanInfoviewService.automaticallyRefreshInternalInfoview = !leanInfoviewService.automaticallyRefreshInternalInfoview
-        if (!leanInfoviewService.automaticallyRefreshInternalInfoview) {
-            e.presentation.isEnabled = false
-        } else {
-            e.presentation.isEnabled = true
-        }
-    }
-
-    override fun getActionUpdateThread(): ActionUpdateThread {
-        return ActionUpdateThread.BGT
-    }
-}

src/main/kotlin/lean4ij/actions/ToggleAutomaticallyRefreshInternalInfoview.kt

@@ -0,0 +1,39 @@
+package lean4ij.actions
+
+import com.intellij.icons.AllIcons
+import com.intellij.openapi.actionSystem.ActionUpdateThread
+import com.intellij.openapi.actionSystem.AnAction
+import com.intellij.openapi.actionSystem.AnActionEvent
+import com.intellij.openapi.components.service
+import com.intellij.openapi.util.IconLoader
+import lean4ij.infoview.LeanInfoviewService
+import javax.swing.Icon
+
+/**
+ * TODO maybe add some buttons/actions for stop/start/toggle automatically refreshing the infoview
+ *      which turn it into a manual mode
+ */
+class ToggleAutomaticallyRefreshInternalInfoview : AnAction() {
+
+    private val onIcon: Icon = IconLoader.getIcon("/icons/textAutoGenerate.svg", javaClass)
+    private val offIcon: Icon = AllIcons.Actions.Suspend
+    init {
+        templatePresentation.icon = onIcon
+        templatePresentation.disabledIcon = offIcon
+    }
+
+    override fun actionPerformed(e: AnActionEvent) {
+        val project = e.project?:return
+        val leanInfoviewService = project.service<LeanInfoviewService>()
+        leanInfoviewService.automaticallyRefreshInternalInfoview = !leanInfoviewService.automaticallyRefreshInternalInfoview
+        if (!leanInfoviewService.automaticallyRefreshInternalInfoview) {
+            e.presentation.isEnabled = false
+        } else {
+            e.presentation.isEnabled = true
+        }
+    }
+
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT
+    }
+}

src/main/kotlin/lean4ij/actions/ToggleLeanInfoViewInternal.kt

@@ -41,7 +41,7 @@
     }
 
     override fun update(e: AnActionEvent) {
         val editor = e.dataContext.getData<Editor>(CommonDataKeys.EDITOR)?:return
         if (!LeanUtil.isLeanFile(editor.virtualFile)) {
             e.presentation.isVisible = false
         }
@@ -61,7 +61,7 @@
     }
 
     override fun getActionUpdateThread(): ActionUpdateThread {
         return ActionUpdateThread.BGT;
     }
 }
 
@@ -144,7 +144,7 @@
     }
 
     init {
         templatePresentation.icon = getIcon("/icons/review_eye.svg", javaClass);
     }
 
     override fun actionPerformed(e: AnActionEvent) {
@@ -164,7 +164,7 @@
     }
 
     init {
         templatePresentation.icon = getIcon("/icons/review_eye.svg", javaClass);
     }
 
     /**
@@ -186,7 +186,7 @@
 class ToggleInternalInfoviewSoftWrap : AbstractToggleUseSoftWrapsAction(SoftWrapAppliancePlaces.MAIN_EDITOR, false) {
 
     init {
         templatePresentation.icon = getIcon("/icons/newLine.svg", javaClass);
 
         // TODO not sure if it should call the method copy from, but
         //      it make the text into 'Soft-Wrap', which is wrong and cannot distinguish from the builtin action
@@ -194,7 +194,7 @@
     }
 
     override fun getActionUpdateThread(): ActionUpdateThread {
         return ActionUpdateThread.BGT;
     }
 
     override fun getEditor(e: AnActionEvent): Editor? {
@@ -219,7 +219,7 @@
     private val toggleLeanInfoViewJcef = ActionManager.getInstance().getAction("ToggleLeanInfoViewJcef")
 
     override fun getActionUpdateThread(): ActionUpdateThread {
         return ActionUpdateThread.BGT;
     }
 
     override fun actionPerformed(e: AnActionEvent) {
@@ -239,4 +239,5 @@
             e.presentation.isVisible = false
         }
     }
-}
+}
+

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

@@ -34,14 +34,19 @@
     /**
      * This si for displaying popup expr
      */
     val popupEditor : CompletableDeferred<EditorEx> = CompletableDeferred()
     val project = toolWindow.project
     val leanProject = project.service<LeanProjectService>()
     val leanInfoviewService = project.service<LeanInfoviewService>()
     init {
         leanProject.scope.launch(Dispatchers.EDT) {
             try {
                 val editor0 = createEditor()
+                // There are many ways to do this
+                // one is ths contextMenuGroup, or handle it manually with installPopupHandler
+                // or using things like PopupHandler.installPopupMenu
+                // check: https://intellij-support.jetbrains.com/hc/en-us/community/posts/6912597187218-How-can-I-create-a-custom-right-click-menu-that-contains-a-couple-of-actions-and-attach-the-menu-to-each-element-in-a-JTree-in-my-plugin
+                // and  https://github.com/JetBrains/intellij-community/blob/master/platform/lang-impl/src/com/intellij/packageDependencies/ui/DependenciesPanel.java
                 editor0.contextMenuGroupId = "lean4ij.infoview.rightClickGroup"
                 editor0.installPopupHandler { event ->
                     val leanInfoviewService = project.service<LeanInfoviewService>()
@@ -65,10 +70,10 @@
         leanInfoviewService.toolWindow = this
     }
 
     private val BORDER = BorderFactory.createEmptyBorder(3, 0, 5, 0)
 
     // TODO
     private fun render(map: Map<*, *>): String {
         for (g in map["goals"] as List<*>) {
             return ""
         }
@@ -100,7 +105,7 @@
                 additionalLinesCount = 0
                 additionalColumnsCount = 1
                 isVirtualSpace = false
                 if (isPopupDoc) {
                     // for popup doc of inline infoview, the folding outline should not be shown
                     isFoldingOutlineShown = false
                 } else {

src/main/kotlin/lean4ij/infoview/external/ExternalInfoViewService.kt

@@ -38,6 +38,7 @@
 /**
  * External infoview service, bridging the http service and the lean project service
  * TODO maybe switch to intellij's extension point to remove ktor for reducing plugin size
+ * TODO should this be merged with [JcefInfoviewService]?
  */
 @Service(Service.Level.PROJECT)
 class ExternalInfoViewService(val project: Project) {
@@ -161,7 +162,7 @@
         return events.asSharedFlow()
     }
 
     private val scope = CoroutineScope(Dispatchers.IO)
 
     suspend fun getSession(uri: String) : String = leanProjectService.getSession(uri)
 
@@ -172,7 +173,7 @@
     /**
      * TODO determine the return type
      */
     suspend fun applyEdit(params: ApplyEditParam): JsonElement? {
         for (change in params.changes) {
             leanProjectService.file(change.key).applyEdit(change.value)
         }

src/main/kotlin/lean4ij/infoview/external/JcefInfoviewTooWindowFactory.kt

@@ -1,7 +1,6 @@
 package lean4ij.infoview.external
 
 import com.intellij.ide.BrowserUtil
-import com.intellij.openapi.actionSystem.ActionGroup
 import com.intellij.openapi.actionSystem.ActionManager
 import com.intellij.openapi.actionSystem.ActionToolbar
 import com.intellij.openapi.actionSystem.DefaultActionGroup
@@ -14,11 +13,16 @@
 import com.intellij.openapi.wm.ToolWindow
 import com.intellij.openapi.wm.ToolWindowFactory
 import com.intellij.openapi.wm.ToolWindowManager
+import com.intellij.ui.DocumentAdapter
+import com.intellij.ui.SearchTextField
 import com.intellij.ui.content.ContentFactory
 import com.intellij.ui.dsl.builder.panel
 import com.intellij.ui.jcef.JBCefApp
 import com.intellij.ui.jcef.JBCefBrowser
 import com.intellij.util.ui.JBUI
+import kotlinx.coroutines.channels.Channel
+import kotlinx.coroutines.launch
+import lean4ij.util.leanProjectScope
 import lean4ij.util.notify
 import org.cef.browser.CefBrowser
 import org.cef.browser.CefFrame
@@ -31,13 +35,78 @@
 import org.cef.network.CefRequest
 import org.cef.security.CefSSLInfo
 import java.awt.BorderLayout
-import javax.swing.JComponent
+import java.awt.event.KeyAdapter
+import java.awt.event.KeyEvent
+import javax.swing.event.DocumentEvent
 
 /**
  * TODO the name like infoview and infoView is inconsistent in the whole codebase...
  */
 @Service(Service.Level.PROJECT)
 class JcefInfoviewService(private val project: Project) {
+    /**
+     * Still cannot add case-sensitive, up and down search
+     * - https://github.com/JetBrains/intellij-plugins/blob/master/qodana/core/src/org/jetbrains/qodana/ui/link/LinkCloudProjectView.kt
+     * - https://github.com/plaskowski/EmbeddedBrowserIntellijPlugin/blob/main/src/main/kotlin/com/github/plaskowski/embeddedbrowserintellijplugin/ui/TextFieldAction.kt
+     *
+     * may help
+     */
+    val searchTextField : SearchTextField = SearchTextField()
+    val searchTextFlow: Channel<String> = Channel()
+
+    init {
+        searchTextField.isVisible = false
+        searchTextField.addDocumentListener(object: DocumentAdapter() {
+            override fun textChanged(e: DocumentEvent) {
+                project.leanProjectScope.launch {
+                    searchTextFlow.send(searchTextField.text)
+                }
+            }
+        })
+        searchTextField.addKeyboardListener(object : KeyAdapter() {
+            private fun searchDown() {
+                val text = searchTextField.text
+                if (text.isNotEmpty()) {
+                    browser?.cefBrowser?.find(text, true, false, true)
+                }
+            }
+
+            private fun searchUp() {
+                val text = searchTextField.text
+                if (text.isNotEmpty()) {
+                    browser?.cefBrowser?.find(text, false, false, true)
+                }
+                return
+            }
+
+            override fun keyReleased(e: KeyEvent) {
+                when {
+                    e.keyCode == KeyEvent.VK_ENTER && !e.isShiftDown -> searchDown()
+                    e.keyCode == KeyEvent.VK_DOWN -> searchDown()
+                    e.keyCode == KeyEvent.VK_ENTER && e.isShiftDown -> searchUp()
+                    e.keyCode == KeyEvent.VK_UP -> searchUp()
+                    e.keyCode == KeyEvent.VK_ESCAPE -> {
+                        searchTextField.isVisible = false
+                        project.leanProjectScope.launch {
+                            searchTextFlow.send("")
+                        }
+                    }
+                }
+            }
+        })
+        project.leanProjectScope.launch {
+            // TODO should this be stopped sometime? like many other infinite loops
+            while (true) {
+                val text = searchTextFlow.receive()
+                if (text.isEmpty()) {
+                    browser?.cefBrowser?.stopFinding(true)
+                } else {
+                    browser?.cefBrowser?.find(text, true, false, false)
+                }
+            }
+        }
+    }
+
     var actionToolbar: ActionToolbar? = null
     private var _url: String? = null
     val url get() = _url
@@ -75,7 +144,7 @@
         }
         browser.zoomLevel = defaultZoomLevel!!
     }
     var defaultZoomLevel: Double? = null
 
     val errMsg =
         "JCEF is unsupported. It maybe the IDE is started with an alternative JDK that does not include JCEF or Its version is not compatible with the running IDE."
@@ -92,8 +161,8 @@
                     browser: CefBrowser?,
                     frame: CefFrame?,
                     request: CefRequest?,
                     user_gesture: Boolean,
                     is_redirect: Boolean
                 ): Boolean {
                     if (request == null) return false
                     val isInfoview = request.url.startsWith(_url!!)
@@ -108,8 +177,8 @@
                 override fun onOpenURLFromTab(
                     browser: CefBrowser?,
                     frame: CefFrame?,
                     target_url: String?,
                     user_gesture: Boolean
                 ): Boolean {
                     return false
                 }
@@ -128,7 +197,7 @@
 
                 override fun getAuthCredentials(
                     browser: CefBrowser?,
                     origin_url: String?,
                     isProxy: Boolean,
                     host: String?,
                     port: Int,
@@ -141,8 +210,8 @@
 
                 override fun onCertificateError(
                     browser: CefBrowser?,
                     cert_error: CefLoadHandler.ErrorCode?,
                     request_url: String?,
                     sslInfo: CefSSLInfo?,
                     callback: CefCallback?
                 ): Boolean {
@@ -178,6 +247,11 @@
         val jcefService = project.service<JcefInfoviewService>()
         val browser = jcefService.browser
         if (browser != null) {
+            // There is a concept named speed search built in list or tree etc.
+            // see: https://plugins.jetbrains.com/docs/intellij/search-field.html#icons
+            // and maybe things like com.intellij.ui.speedSearch.SpeedSearchSupply
+            // and com.intellij.openapi.wm.impl.welcomeScreen.recentProjects.RecentProjectFilteringTree
+            browser.component.add(jcefService.searchTextField, BorderLayout.NORTH)
             jcefInfoview.add(browser.component)
         } else {
             jcefInfoview.add(panel {
@@ -189,7 +263,7 @@
         jcefService.actionToolbar = configureToolbar(project, toolWindow)
     }
 
     fun configureToolbar(project: Project, toolWindow: ToolWindow): ActionToolbar {
         val actions = DefaultActionGroup()
         val manager = ActionManager.getInstance()
         actions.add(manager.getAction("RestartJcefInfoview"))
@@ -200,6 +274,7 @@
         actions.add(manager.getAction("DecreaseZoomLevelForLeanInfoViewJcef"))
         actions.add(manager.getAction("ResetZoomLevelForLeanInfoViewJcef"))
         actions.add(manager.getAction("ToggleLeanInfoviewJcefToolbarVisibility"))
+        actions.add(manager.getAction("FindInExternalInfoview"))
 
         // TODO what is place for?
         val tb = manager.createActionToolbar("Lean Jcef Infoview", actions, true)

src/main/kotlin/lean4ij/util/ProjectUtil.kt

@@ -1,10 +1,11 @@
 package lean4ij.util
 
 import com.intellij.notification.Notification
-import com.intellij.notification.NotificationGroupManager
-import com.intellij.notification.NotificationGroupManager.*
+import com.intellij.notification.NotificationGroupManager.getInstance
 import com.intellij.notification.NotificationType
+import com.intellij.openapi.components.service
 import com.intellij.openapi.project.Project
+import lean4ij.project.LeanProjectService
 
 
 /**
@@ -15,7 +16,7 @@
         // TODO custom notification group
         .getNotificationGroup("Custom Notification Group")
         .createNotification(content, NotificationType.ERROR)
         .notify(this);
 }
 
 fun Project.notify(content: String) {
@@ -23,21 +24,25 @@
         // TODO custom notification group
         .getNotificationGroup("Custom Notification Group")
         .createNotification(content, NotificationType.INFORMATION)
         .notify(this);
 }
 
 fun Project.notify(content: String, type: NotificationType) {
     getInstance()
         // TODO custom notification group
         .getNotificationGroup("Custom Notification Group")
         .createNotification(content, type)
         .notify(this);
 }
 
 fun Project.notify(content: String, action: (Notification) -> Notification) {
     val notification = getInstance()
         // TODO custom notification group
         .getNotificationGroup("Custom Notification Group")
         .createNotification(content, NotificationType.INFORMATION)
     action(notification)
-}
+}
+
+val Project.leanProjectService get(): LeanProjectService = service()
+
+val Project.leanProjectScope get() = leanProjectService.scope

src/main/resources/META-INF/plugin.xml

@@ -212,6 +212,10 @@
             <add-to-group group-id="MainMenu" anchor="last"/>
         </action>
 
+        <action id="FindInExternalInfoview" class="lean4ij.actions.FindInExternalInfoview" text="Find in external infoview" description="Find in external infoview">
+            <add-to-group group-id="MainMenu" anchor="last"/>
+        </action>
+
         <group id="lean4ij.infoview.rightClickGroup" text="Infoview Right click Actions" popup="true"/>
 
         <action id="InternalInfoviewGotoDefinition" class="lean4ij.actions.InternalInfoviewGotoDefinition" text="Go to Definition" description="InternalInfoviewGotoDefinition">