some more heuristic highlight

gradle.properties

@@ -14,8 +14,9 @@ pluginSinceBuild = 241
 # pluginUntilBuild = 242.*
 
 # IntelliJ Platform Properties -> https://plugins.jetbrains.com/docs/intellij/tools-gradle-intellij-plugin.html#configuration-intellij-extension
-platformType = IU
-platformVersion = 2024.2
+# TODO it seems the tests failed in IU 2024.2
+platformType = IC
+platformVersion = 2024.1
 
 # Plugin Dependencies -> https://plugins.jetbrains.com/docs/intellij/plugin-dependencies.html
 # Example: platformPlugins = com.intellij.java, com.jetbrains.php:203.4449.22

src/main/grammars/Lean4Lexer.flex

@@ -56,9 +56,9 @@ KEYWORD_COMMAND_PREFIX   = local|private|protected|scoped|partial|noncomputable|
 KEYWORD_MODIFIER        = renaming|hiding|where|extends|using|with|at|rec|deriving
 KEYWORD_COMMAND2        = syntax|elab|elab_rules|macro_rules|macro
 KEYWORD_COMMAND3        = namespace|section|end
-KEYWORD_COMMAND4        = class|def|lemma|example|theorem|instance|structure
-KEYWORD_COMMAND5        = #check|#guard_msgs|#eval|#reduce
-KEYWORD_COMMAND6        = match|have|with|by
+KEYWORD_COMMAND4        = class|def|lemma|example|theorem|instance|structure|fun|set_option|vairable
+KEYWORD_COMMAND5        = #check|#guard_msgs|#eval|#reduce|#synth|#help
+KEYWORD_COMMAND6        = match|have|with|by|in
 KEYWORD_SORRY = sorry
 DEFAUTL_TYPE = Type|(Type \*)
 
@@ -222,6 +222,9 @@ nhaddock_start      = {left_brace}{dash}{white_char}?{vertical_bar}
     {at} {
         return AT;
     }
+    {underscore} {
+        return PLACEHOLDER;
+    }
     {at_leftbracket}        {
         return ATTRIBUTE_START;
     }

src/main/grammars/Lean4Parser.bnf

@@ -14,7 +14,7 @@
     elementTypeClass = "lean4ij.language.Lean4TokenType"
 }
 
-tokens ::= (WHITE_SPACE|
+tokens ::= (
     LINE_COMMENT|
     STRING|
     KEYWORD_COMMAND1|
@@ -52,6 +52,7 @@ tokens ::= (WHITE_SPACE|
     KEYWORD_SORRY|
     TEMPLATE_TRIGGER|
     ASSIGN|
+    PLACEHOLDER|
     definition|
     attributes
     )*

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

@@ -1,6 +1,7 @@
 package lean4ij.actions
 
 import com.intellij.ide.BrowserUtil
+import com.intellij.openapi.actionSystem.ActionUpdateThread
 import com.intellij.openapi.actionSystem.AnAction
 import com.intellij.openapi.actionSystem.AnActionEvent
 import com.intellij.openapi.actionSystem.CommonDataKeys
@@ -52,6 +53,9 @@ class ToggleLeanInfoViewJcef : AnAction() {
         }
     }
 
+    override fun getActionUpdateThread(): ActionUpdateThread {
+        return ActionUpdateThread.BGT;
+    }
 }
 
 class OpenExternalInfoviewInBrowser : AnAction() {

src/main/kotlin/lean4ij/language/Lean4ParserDefinition.kt

@@ -15,6 +15,7 @@ import com.intellij.openapi.project.Project
 import com.intellij.psi.FileViewProvider
 import com.intellij.psi.PsiElement
 import com.intellij.psi.PsiFile
+import com.intellij.psi.TokenType.WHITE_SPACE
 import com.intellij.psi.tree.IElementType
 import com.intellij.psi.tree.IFileElementType
 import com.intellij.psi.tree.TokenSet
@@ -37,6 +38,7 @@ class Lean4ParserDefinition : ParserDefinition {
         val FILE = IFileElementType(Lean4Language.INSTANCE)
         val COMMENTS = TokenSet.create(LINE_COMMENT, DOC_COMMENT, BLOCK_COMMENT)
         val STRINGS = TokenSet.create(STRING)
+        val WHITESPACE = TokenSet.create(WHITE_SPACE)
     }
 
     override fun createLexer(project: Project?): Lexer = Lean4LexerAdapter()
@@ -47,6 +49,8 @@ class Lean4ParserDefinition : ParserDefinition {
 
     override fun getCommentTokens(): TokenSet = COMMENTS
 
+    override fun getWhitespaceTokens(): TokenSet = WHITESPACE
+
     override fun getStringLiteralElements(): TokenSet = STRINGS
 
     override fun createElement(node: ASTNode): PsiElement {

src/main/kotlin/lean4ij/language/Lean4SyntaxHighlighter.kt

@@ -5,6 +5,7 @@ import com.intellij.lang.annotation.AnnotationHolder
 import com.intellij.lang.annotation.Annotator
 import com.intellij.lang.annotation.HighlightSeverity
 import com.intellij.lexer.Lexer
+import com.intellij.openapi.components.service
 import com.intellij.openapi.editor.DefaultLanguageHighlighterColors
 import com.intellij.openapi.editor.HighlighterColors.BAD_CHARACTER
 import com.intellij.openapi.editor.colors.TextAttributesKey
@@ -15,7 +16,10 @@ import com.intellij.openapi.fileTypes.SyntaxHighlighterFactory
 import com.intellij.openapi.project.Project
 import com.intellij.openapi.vfs.VirtualFile
 import com.intellij.psi.PsiElement
+import com.intellij.psi.TokenType.WHITE_SPACE
 import com.intellij.psi.tree.IElementType
+import com.intellij.psi.util.elementType
+import lean4ij.Lean4Settings
 import lean4ij.language.psi.TokenType
 import java.nio.charset.StandardCharsets
 
@@ -89,6 +93,7 @@ class Lean4SyntaxHighlighterFactory : SyntaxHighlighterFactory() {
  * TODO use customized text attributes
  */
 class Lean4Annotator : Annotator {
+    private val lean4Settings = service<Lean4Settings>()
 
     companion object {
         val tactics = getAllTactics()
@@ -113,9 +118,8 @@ class Lean4Annotator : Annotator {
                 holder.newSilentAnnotation(HighlightSeverity.INFORMATION)
                     .range(element.textRange).textAttributes(DefaultLanguageHighlighterColors.FUNCTION_DECLARATION).create();
             }
-        }
-        // check the parent rather than the element itself for skipping comments
-        if (element.parent is Lean4Attributes) {
+        } else if (element.parent is Lean4Attributes) {
+            // check the parent rather than the element itself for skipping comments
             if (element.node.elementType == TokenType.IDENTIFIER) {
                 holder.newSilentAnnotation(HighlightSeverity.INFORMATION)
                     .range(element.textRange).textAttributes(DefaultLanguageHighlighterColors.METADATA).create();
@@ -124,12 +128,38 @@ class Lean4Annotator : Annotator {
                 holder.newSilentAnnotation(HighlightSeverity.INFORMATION)
                     .range(element.textRange).textAttributes(DefaultLanguageHighlighterColors.KEYWORD).create();
             }
-        }
-        if (element.node.elementType == TokenType.IDENTIFIER) {
-            if (tactics.containsKey(element.text)) {
+        } else if (element.node.elementType == TokenType.IDENTIFIER) {
+            if (isField(element)) {
                 holder.newSilentAnnotation(HighlightSeverity.INFORMATION)
-                    .range(element.textRange).textAttributes(DefaultLanguageHighlighterColors.FUNCTION_CALL).create();
+                    .range(element.textRange).textAttributes(DefaultLanguageHighlighterColors.INSTANCE_FIELD).create();
+            } else {
+                if (tactics.containsKey(element.text)) {
+                    holder.newSilentAnnotation(HighlightSeverity.INFORMATION)
+                        .range(element.textRange).textAttributes(DefaultLanguageHighlighterColors.FUNCTION_CALL).create();
+                }
             }
         }
     }
+
+    private fun isField(element: PsiElement): Boolean {
+        return prevSiblingIsNewLine(element) && nextSiblingIsAssign(element)
+    }
+
+    private fun prevSiblingIsNewLine(element: PsiElement): Boolean {
+        val prevElement = element.prevSibling?:return false
+        return prevElement.elementType == WHITE_SPACE && prevElement.text.contains('\n')
+    }
+
+    private fun nextSiblingIsAssign(element: PsiElement): Boolean {
+        var nextValidElement : PsiElement? = element.nextSibling
+        while (!isValid(nextValidElement)) {
+            nextValidElement = nextValidElement?.nextSibling
+        }
+        val elementType = nextValidElement?.node?.elementType
+        return elementType == TokenType.ASSIGN || elementType == TokenType.COLON
+    }
+
+    private fun isValid(element: PsiElement?): Boolean {
+        return element?.node?.elementType != WHITE_SPACE && element?.node?.elementType != TokenType.PLACEHOLDER;
+    }
 }