diff --git a/TODO.md b/TODO.md index 206f3d6..ab84f8d 100644 --- a/TODO.md +++ b/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 + carrior : Set M +``` \ No newline at end of file diff --git a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt b/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt index a216043..6196245 100644 --- a/src/main/kotlin/lean4ij/infoview/LeanInfoViewWindowFactory.kt +++ b/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) diff --git a/src/main/kotlin/lean4ij/infoview/LeanInfoviewColorSettingPage.kt b/src/main/kotlin/lean4ij/infoview/LeanInfoviewColorSettingPage.kt index 0c697db..99e007e 100644 --- a/src/main/kotlin/lean4ij/infoview/LeanInfoviewColorSettingPage.kt +++ b/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), } diff --git a/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt b/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt index c10a4e0..250b231 100644 --- a/src/main/kotlin/lean4ij/language/InfoviewInlayHintsProviderFactory.kt +++ b/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 diff --git a/src/main/kotlin/lean4ij/project/LeanFile.kt b/src/main/kotlin/lean4ij/project/LeanFile.kt index d14e686..004e694 100644 --- a/src/main/kotlin/lean4ij/project/LeanFile.kt +++ b/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() + private val diagnosticsChannel = run { + val channel = Channel() + leanProjectService.scope.launch { + this@LeanFile.getAllMessages(channel) + } + channel + } + private var allMessage : List? = null - private suspend fun getAllMessages() { + private suspend fun getAllMessages(channel: Channel) { 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) {