some fix

TODO.md

@@ -40,3 +40,21 @@
 - [ ] unify jcef/browser/external/vscode infoview font name...
 - [ ] jcef infoview popup link should be opened in external web browser
 - [ ] setting page
+  - [x] added a setting page
+  - [ ] add some other settings
+- [ ] line comment and block comment
+- [ ] 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 step? first show alphabet autocompletion and then add more semantic 
+  autocompletion 
+- [ ] quick fix for field missing
+- [ ] color for error message
+- [ ] code completion seems slow and requires manually press ctrl+space
+- [ ] TODO is not highlight
+
+# Maybe some improvements
+
+it is not automatically indent:
+```lean
+structure Submonoid₁ (M : Type) [Monoid M] where<ENTER HERE DOES NOT INTENT>
+  carrior : Set M
+```

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

@@ -124,7 +124,19 @@ class LeanInfoViewWindowFactory : ToolWindowFactory {
                     } else {
                         // TODO for TaggedTextAppend there is also case for not supported trace
                         val content = i.message.toInfoViewString(infoviewRender, null)
-                        infoviewRender.highlight(start, end1, TextAttributesKeys.SwingInfoviewAllMessagePos)
+                        // TODO remove this magic number and define some enum for it
+                        //      instance : ToJson DiagnosticSeverity := ⟨fun
+                        //      | DiagnosticSeverity.error       => 1
+                        //      | DiagnosticSeverity.warning     => 2
+                        //      | DiagnosticSeverity.information => 3
+                        //      | DiagnosticSeverity.hint        => 4⟩
+                        //  check src/Lean/Data/Lsp/Diagnostics.lean
+                        var key = if (i.severity == 1) {
+                            TextAttributesKeys.SwingInfoviewAllMessageErrorPos
+                        } else {
+                            TextAttributesKeys.SwingInfoviewAllMessagePos
+                        }
+                        infoviewRender.highlight(start, end1, key)
                     }
                     val end2 = infoviewRender.length
                     infoviewRender.addFoldingOperation(start, end2, header)

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

@@ -3,6 +3,7 @@ package lean4ij.infoview
 import com.intellij.openapi.diff.DiffColors
 import com.intellij.openapi.editor.DefaultLanguageHighlighterColors
 import com.intellij.openapi.editor.HighlighterColors
+import com.intellij.openapi.editor.colors.CodeInsightColors
 import com.intellij.openapi.editor.colors.TextAttributesKey
 import com.intellij.openapi.fileTypes.PlainSyntaxHighlighter
 import com.intellij.openapi.fileTypes.SyntaxHighlighter
@@ -40,6 +41,7 @@ enum class TextAttributesKeys(val style: String, private val fallbackKey: TextAt
     SwingInfoviewGoalSymbol("swing-infoview-goal-symbol", DefaultLanguageHighlighterColors.STRING, AttrSelect.ALL),
     SwingInfoviewCasePos("swing-infoview-case-pos", DefaultLanguageHighlighterColors.HIGHLIGHTED_REFERENCE, AttrSelect.ALL),
     SwingInfoviewAllMessagePos("swing-infoview-all-message-pos", DefaultLanguageHighlighterColors.FUNCTION_DECLARATION, AttrSelect.ALL),
+    SwingInfoviewAllMessageErrorPos("swing-infoview-all-message-error-pos", CodeInsightColors.RUNTIME_ERROR, AttrSelect.ALL),
     SwingInfoviewAllMessageSorryPos("swing-infoview-all-message-sorry-pos", DefaultLanguageHighlighterColors.INVALID_STRING_ESCAPE, AttrSelect.ALL),
     SwingInfoviewAllMessageUnsupportedPos("swing-infoview-all-message-unsupported-pos", HighlighterColors.BAD_CHARACTER, AttrSelect.ALL),
 }

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

@@ -251,7 +251,8 @@ class PlaceHolderInlayHintsCollector(editor: Editor, project: Project?) : InlayH
             val position = org.eclipse.lsp4j.Position(lineColumn.line, lineColumn.column)
             val textDocument = TextDocumentIdentifier(LspUtil.quote(file.virtualFile!!.path))
             val hover = languageServer.hover(HoverParams(textDocument, position)).await()
-            if (hover.contents.isRight) {
+            // TODO there are cases here that here hover is null
+            if (hover != null && hover.contents.isRight) {
                 val value = hover.contents.right.value
                 if (value.contains("placeholder")) {
                     // TODO assume that only one line..., this maybe wrong

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

@@ -128,9 +128,10 @@ class LeanFile(private val leanProjectService: LeanProjectService, private val f
                 buildWindowService.endBuild(file)
             }
         }
-        scope.launch {
-            getAllMessages()
-        }
+        // it seems facing some initialization order problem
+        // scope.launch {
+        //     getAllMessages()
+        // }
     }
 
     /**
@@ -407,16 +408,25 @@ class LeanFile(private val leanProjectService: LeanProjectService, private val f
 
     /**
      * TODO can this be replaced with flow?
+     * TODO this form is changed from a initialization order error
+     *      that getAllMessages run before it init
      */
-    private val diagnosticsChannel = Channel<Diagnostic>()
+    private val diagnosticsChannel = run {
+        val channel = Channel<Diagnostic>()
+        leanProjectService.scope.launch {
+            this@LeanFile.getAllMessages(channel)
+        }
+        channel
+    }
+
     private var allMessage : List<InteractiveDiagnostics>? = null
 
-    private suspend fun getAllMessages() {
+    private suspend fun getAllMessages(channel: Channel<Diagnostic>) {
         var maxLine = -1
          while (true) {
              try {
                  val diagnostic = withTimeout(1*1000) {
-                      diagnosticsChannel.receive()
+                      channel.receive()
                  }
                  maxLine = max(maxLine, diagnostic.range.end.line)
              } catch (ex: TimeoutCancellationException) {