tuning icons, instantly update internal infoview and open links of ex…

…ternal infoview in browser

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

@@ -1,5 +1,6 @@
 package lean4ij.infoview.external
 
+import com.intellij.ide.BrowserUtil
 import com.intellij.openapi.components.Service
 import com.intellij.openapi.components.service
 import com.intellij.openapi.diagnostic.thisLogger
@@ -12,7 +13,20 @@ 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.ui.jcef.JBCefClient
 import lean4ij.util.notify
+import org.cef.CefSettings
+import org.cef.browser.CefBrowser
+import org.cef.browser.CefFrame
+import org.cef.callback.CefAuthCallback
+import org.cef.callback.CefCallback
+import org.cef.handler.CefDisplayHandler
+import org.cef.handler.CefLoadHandler
+import org.cef.handler.CefRequestHandler
+import org.cef.handler.CefResourceRequestHandler
+import org.cef.misc.BoolRef
+import org.cef.network.CefRequest
+import org.cef.security.CefSSLInfo
 
 /**
  * TODO the name like infoview and infoView is inconsistent in the whole codebase...
@@ -62,6 +76,78 @@ class JcefInfoviewService(private val project: Project) {
     val browser: JBCefBrowser? = if (JBCefApp.isSupported()) {
         val browser = JBCefBrowser()
         defaultZoomLevel = browser.zoomLevel
+
+        // handle link clicks, which should be opened in real browser but not jcef
+
+        browser.jbCefClient
+            .addRequestHandler(object : CefRequestHandler {
+                override fun onBeforeBrowse(
+                    browser: CefBrowser?,
+                    frame: CefFrame?,
+                    request: CefRequest?,
+                    user_gesture: Boolean,
+                    is_redirect: Boolean
+                ): Boolean {
+                    if (request == null) return false
+                    val isInfoview = request.url.startsWith(_url!!)
+                    if (isInfoview) {
+                        return false
+                    } else {
+                        BrowserUtil.browse(request.url)
+                        return true
+                    }
+                }
+
+                override fun onOpenURLFromTab(
+                    browser: CefBrowser?,
+                    frame: CefFrame?,
+                    target_url: String?,
+                    user_gesture: Boolean
+                ): Boolean {
+                    return false
+                }
+
+                override fun getResourceRequestHandler(
+                    browser: CefBrowser?,
+                    frame: CefFrame?,
+                    request: CefRequest?,
+                    isNavigation: Boolean,
+                    isDownload: Boolean,
+                    requestInitiator: String?,
+                    disableDefaultHandling: BoolRef?
+                ): CefResourceRequestHandler? {
+                    return null
+                }
+
+                override fun getAuthCredentials(
+                    browser: CefBrowser?,
+                    origin_url: String?,
+                    isProxy: Boolean,
+                    host: String?,
+                    port: Int,
+                    realm: String?,
+                    scheme: String?,
+                    callback: CefAuthCallback?
+                ): Boolean {
+                    return false
+                }
+
+                override fun onCertificateError(
+                    browser: CefBrowser?,
+                    cert_error: CefLoadHandler.ErrorCode?,
+                    request_url: String?,
+                    sslInfo: CefSSLInfo?,
+                    callback: CefCallback?
+                ): Boolean {
+                    return false
+                }
+
+                override fun onRenderProcessTerminated(
+                    browser: CefBrowser?,
+                    status: CefRequestHandler.TerminationStatus?
+                ) {
+                }
+            }, browser.cefBrowser )
         browser
     } else {
         // TODO make this shorter

src/main/kotlin/lean4ij/project/LeanFile.kt

@@ -204,6 +204,8 @@ class LeanFile(private val leanProjectService: LeanProjectService, private val f
      *      more smoothly and independently
      * TODO maybe try psi for infoview tool window
      * TODO passing things like editor etc seems cumbersome, maybe add some implement for context
+     * TODO this should maybe named as [updateInternalInfoview], but it contains a switch...
+     *      The switch should put in [updateInternalInfoview]
      */
     fun updateCaret(editor: Editor, logicalPosition: LogicalPosition) {
         if (lean4Settings.enableNativeInfoview) {
@@ -455,13 +457,24 @@ class LeanFile(private val leanProjectService: LeanProjectService, private val f
                         position
                     )
                     allMessage = getInteractiveDiagnostics(diagnosticsParams)
+                    // after getting all Messages, do an update intermediately...
+                    // to avoid lag
+                    updateCaretIntermediately()
                     lastMaxLine = maxLine
                     maxLine = -1
                 }
             }
         }
     }
 
+    private fun updateCaretIntermediately() {
+        FileEditorManager.getInstance(project).selectedTextEditor?.let { editor ->
+            if (editor.virtualFile.path == unquotedFile) {
+                updateCaret(editor, editor.caretModel.logicalPosition)
+            }
+        }
+    }
+
     /**
      * checking a bug for all messages not updated correctly. It shows that there is a cases like:
      * [Trace - 10:59:11] Received notification 'textDocument/publishDiagnostics'

src/main/kotlin/lean4ij/project/LeanProjectActivity.kt

@@ -6,6 +6,9 @@ import com.intellij.openapi.components.service
 import com.intellij.openapi.diagnostic.thisLogger
 import com.intellij.openapi.editor.Editor
 import com.intellij.openapi.editor.EditorFactory
+import com.intellij.openapi.editor.LogicalPosition
+import com.intellij.openapi.editor.event.DocumentEvent
+import com.intellij.openapi.editor.event.DocumentListener
 import com.intellij.openapi.editor.ex.EditorEventMulticasterEx
 import com.intellij.openapi.editor.ex.FocusChangeListener
 import com.intellij.openapi.module.ModuleUtilCore
@@ -20,6 +23,11 @@ import com.intellij.openapi.module.Module
 import lean4ij.lsp.LeanLanguageServerFactory
 import lean4ij.util.OsUtil
 import java.awt.event.FocusEvent
+import com.intellij.openapi.fileEditor.FileDocumentManager
+import com.intellij.openapi.util.text.LineColumn
+import com.intellij.openapi.util.text.StringUtil
+import lean4ij.util.LeanUtil
+
 
 fun Module.addExcludeFolder(basePath: String) {
     ModuleRootModificationUtil.updateModel(this) { rootModule ->
@@ -84,7 +92,7 @@ class LeanProjectActivity : ProjectActivity {
 
     override suspend fun execute(project: Project) {
         setupModule(project)
-        setupEditorFocusChangeEventListener()
+        setupEditorFocusChangeEventListener(project)
         project.service<LeanProjectService>()
         project.service<LeanFileCaretListener>()
         project.service<ExternalInfoViewService>()
@@ -96,7 +104,7 @@ class LeanProjectActivity : ProjectActivity {
      *      this is for avoiding didOpen request that make the lean lsp server handling it and improve performance
      *      but it may have some false positive event though
      */
-    private fun setupEditorFocusChangeEventListener() {
+    private fun setupEditorFocusChangeEventListener(project: Project) {
         (EditorFactory.getInstance().eventMulticaster as? EditorEventMulticasterEx)?.let { ex ->
             ex.addFocusChangeListener(object: FocusChangeListener {
                 override fun focusGained(editor: Editor) {
@@ -203,6 +211,27 @@ class LeanProjectActivity : ProjectActivity {
                 //      	at kotlinx.coroutines.scheduling.CoroutineScheduler$Worker.runWorker(CoroutineScheduler.kt:697)
                 //      	at kotlinx.coroutines.scheduling.CoroutineScheduler$Worker.run(CoroutineScheduler.kt:684)
             }
+            // ref: https://intellij-support.jetbrains.com/hc/en-us/community/posts/360006419280-DocumentListener-for-getting-what-line-was-changed
+            // TODO extract DocumentListener
+            ex.addDocumentListener(object : DocumentListener {
+                override fun documentChanged(event: DocumentEvent) {
+                    val document = event.document
+                    val file = FileDocumentManager.getInstance().getFile(document)?:return
+                    if (!LeanUtil.isLeanFile(file)) {
+                        return
+                    }
+                    val leanProjectService = project.service<LeanProjectService>()
+                    val editor = EditorFactory.getInstance().getEditors(document).firstOrNull()?:return
+                    val lineCol : LineColumn = StringUtil.offsetToLineColumn(document.text, event.offset) ?: return
+                    val position = LogicalPosition(lineCol.line, lineCol.column)
+                    // TODO this may be duplicated with caret events some times
+                    //      but without this there are cases no caret events but document changed events
+                    //      maybe some debounce
+                    leanProjectService.file(file).updateCaret(editor, position)
+                }
+            }) {
+                // TODO Disposable
+            }
         }
     }
 

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

@@ -66,7 +66,7 @@
         <!-- check https://plugins.jetbrains.com/docs/intellij/icons.html#mapping-entries for making icons to respect theme -->
         <toolWindow factoryClass="lean4ij.infoview.LeanInfoViewWindowFactory"
                     id="LeanInfoViewWindow"
-                    icon="/icons/lean_icon.svg"
+                    icon="/icons/infoview_icon.svg"
         />
         <toolWindow factoryClass="lean4ij.infoview.external.JcefInfoviewTooWindowFactory"
                     id="LeanInfoviewJcef"