Constructor parameter is never used as a property

Constructor parameter is never used as a property

Constructor parameter is never used as a property

Variable is never modified, so it can be declared using 'val'

Variable is never modified, so it can be declared using 'val'

Variable is never modified, so it can be declared using 'val'

Variable is never modified, so it can be declared using 'val'

'if' has empty body

String '[ref](https://github.com/leanperrover/lean4/tree/master/src/Lean/Server#in-general)' is not properly capitalized. It should have sentence capitalization

Cannot resolve symbol 'CodeWithInfos'

Empty catch block

Unnecessary non-null assertion (!!) on a non-null receiver of type JsonElement

Redundant suppression

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Unused import directive

Explicitly given type is redundant here

'contextInfo' always returns non-null type

'getTextAttributes' always returns non-null type

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant semicolon

Redundant 'suspend' modifier

Redundant visibility modifier

Redundant visibility modifier

Redundant string template

Redundant string template

'LSPDiagnosticFeature()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPDiagnosticFeature' marked with @ApiStatus.Experimental

Overridden method 'isEnabled()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPWorkspaceSymbolFeature' marked with @ApiStatus.Experimental

'LSPCompletionFeature()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPCompletionFeature' marked with @ApiStatus.Experimental

'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' is marked unstable with @ApiStatus.Experimental

'com.redhat.devtools.lsp4ij.client.features.LSPWorkspaceSymbolFeature' is marked unstable with @ApiStatus.Experimental

'getPreferredContentWidth(int)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationEditorPane' marked with @ApiStatus.Internal

'setDiagnosticFeature(com.redhat.devtools.lsp4ij.client.features.@org.jetbrains.annotations.NotNull LSPDiagnosticFeature)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental

Overridden method 'isEnabled(com.intellij.psi.@org.jetbrains.annotations.NotNull PsiFile)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.AbstractLSPDocumentFeature' marked with @ApiStatus.Experimental

'com.intellij.codeInsight.documentation.DocumentationEditorPane' is marked unstable with @ApiStatus.Internal

'com.intellij.codeInsight.documentation.DocumentationScrollPane' is marked unstable with @ApiStatus.Internal

'com.redhat.devtools.lsp4ij.client.features.LSPCompletionFeature' is marked unstable with @ApiStatus.Experimental

'LSPWorkspaceSymbolFeature()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPWorkspaceSymbolFeature' marked with @ApiStatus.Experimental

'com.intellij.codeInsight.documentation.DocumentationScrollPane' is marked unstable with @ApiStatus.Internal

'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' is marked unstable with @ApiStatus.Experimental

'setViewportView(com.intellij.codeInsight.documentation.@org.jetbrains.annotations.NotNull DocumentationEditorPane, javax.swing.@org.jetbrains.annotations.NotNull JLabel)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationScrollPane' marked with @ApiStatus.Internal

Overridden method 'getTextAttributesKey()' is declared in unstable 'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' marked with @ApiStatus.Experimental

'com.intellij.codeInsight.documentation.DocumentationEditorPane' is marked unstable with @ApiStatus.Internal

Overridden method 'getTextAttributesKey()' is declared in unstable 'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' marked with @ApiStatus.Experimental

'LSPClientFeatures()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental

'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' is marked unstable with @ApiStatus.Experimental

'setWorkspaceSymbolFeature(com.redhat.devtools.lsp4ij.client.features.@org.jetbrains.annotations.NotNull LSPWorkspaceSymbolFeature)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental

'setCompletionFeature(com.redhat.devtools.lsp4ij.client.features.@org.jetbrains.annotations.NotNull LSPCompletionFeature)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental

'com.redhat.devtools.lsp4ij.client.features.LSPDiagnosticFeature' is marked unstable with @ApiStatus.Experimental

Overridden method 'isEnabled(com.intellij.openapi.vfs.@org.jetbrains.annotations.NotNull VirtualFile)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental

'setViewportView(com.intellij.codeInsight.documentation.@org.jetbrains.annotations.NotNull DocumentationEditorPane, javax.swing.@org.jetbrains.annotations.NotNull JLabel)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationScrollPane' marked with @ApiStatus.Internal

'com.intellij.openapi.editor.markup.FillingLineMarkerRenderer' is marked unstable with @ApiStatus.Experimental

'getPreferredHeightByWidth(int)' is declared in unstable class 'com.intellij.codeInsight.documentation.DocumentationEditorPane' marked with @ApiStatus.Internal

'getProject()' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.LSPClientFeatures' marked with @ApiStatus.Experimental

Overridden method 'isEnabled(com.intellij.psi.@org.jetbrains.annotations.NotNull PsiFile)' is declared in unstable class 'com.redhat.devtools.lsp4ij.client.features.AbstractLSPDocumentFeature' marked with @ApiStatus.Experimental

Receiver parameter is never used

Function "nextSiblingIsAssign" is never used

Property "term" is never used

Property "collapsed" is never used

Property "project" is never used

Property "isRemoved" is never used

Function "highlight" is never used

Function "updateInteractiveGoal" is never used

Property "BAD_CHAR_KEYS" is never used

Function "plainTermGoal" is never used

Function "updateInfoviewFor" is never used

Function "render" is never used

Function "path" is never used

Function "select" is never used

Property "goalPrefix" is never used

Function "respondSse" is never used

Property "BORDER" is never used

Function "plainGoal" is never used

Property "mvarId" is never used

Class "DiagInlayHintsCollector" is never used

Property "attrSelect" is never used

Property "indent" is never used

Property "height" is never used

Property "onlyManual" is never used

Function "createTextAttributesKey" is never used

Property "SEPARATOR_KEYS" is never used

Function "createExprPanel" is never used

Property "EXTERNAL_INFOVIEW_SERVER_INITIALIZED" is never used

Class "COLOR" is never used

Class "Lean4ElementImpl" is never used

Property "isInserted" is never used

Function "leanFileProgress" is never used

Function "notify" is never used

Function "runCommand" is never used

Property "symbolEntryCache" is never used

Function "onClick" is never used

Function "toJsonElement" is never used

Property "scope" is never used

Property "ctx" is never used

Property "progressingLineMarker" is never used

Object "InfoObjectModelDsl" is never used

Class "FileProgressGutterIconRender" is never used

Property "VALUE_KEYS" is never used

Function "updateGoal" is never used

Property "ctx" is never used

You are running a Qodana linter without an exact version tag: jetbrains/qodana-jvm-community:latest

Cannot run analysis for commit 8c6ac6548c38b14f12bc47bab4d992414197bcfe because it doesn't exist in the repository. Check that you retrieve the full git history before running Qodana.

You are running a Qodana linter without an exact version tag: jetbrains/qodana-jvm-community:latest

You are running a Qodana linter without an exact version tag: jetbrains/qodana-jvm-community:latest

Class name `leanFileProgressFinishedFillingLineMarkerRender` should start with an uppercase letter

Class name `leanFileProgressFillingLineMarkerRender` should start with an uppercase letter

If-Null return/break/... foldable to '?:'

Redundant overriding method

Redundant overriding method

Redundant overriding method

Redundant overriding method

Redundant overriding method

Redundant overriding method

Redundant overriding method

Redundant overriding method

'Return' can be lifted out of 'try'

'Assignment' can be lifted out of 'if'

'Assignment' can be lifted out of 'if'

Local variable name `request_url` should not contain underscores

Local variable name `user_gesture` should not contain underscores

Local variable name `user_gesture` should not contain underscores

Local variable name `cert_error` should not contain underscores

Local variable name `target_url` should not contain underscores

Local variable name `origin_url` should not contain underscores

Local variable name `is_redirect` should not contain underscores

Property 'MAX_LEN' could be private

Function 'createPopupPanel' could be private

Property 'KEY' could be private

Property 'VALUE' could be private

Function 'rpcConnectAsync' could be private

Property 'hyps' could be private

Property 'NUMBER_KEYS' could be private

Property 'SORRY_KEYS' could be private

Function 'getLeanVersion' could be private

Function 'configureToolbar' could be private

Property 'cls' could be private

Property 'leanProject' could be private

Property 'SORRY' could be private

Function 'getInteractiveTermGoalAsync' could be private

Property 'cache' could be private

Function 'rpcCallAsync' could be private

Function 'refresh' could be private

Property 'KEYWORD_IN_PROOF' could be private

Function 'fold' could be private

Function 'fold' could be private

Property 'currentHints' could be private

Property 'popupEditor' could be private

Property 'applyActions' could be private

Function 'getInteractiveGoalsAsync' could be private

Property 'isChangedPredicates' could be private

Function 'plainTermGoalAsync' could be private

Property 'COMMENT_KEYS' could be private

Function 'getHomePath' could be private

Function 'model' could be private

Function 'infoToInteractiveAsync' could be private

Property 'COMMENT' could be private

Function 'createProgress' could be private

Function 'updateHint' could be private

Property 'toolWindow' could be private

Function 'hideHint' could be private

Property 'hintCache' could be private

Function 'lazyTraceChildrenToInteractiveAsync' could be private

Property 'KEY_KEYS' could be private

Property 'NUMBER' could be private

Property 'KEYWORD_IN_PROOF_KEYS' could be private

Function 'plainGoalAsync' could be private

Function 'getInteractiveDiagnosticsAsync' could be private

Property 'EMPTY_KEYS' could be private

Property 'userName' could be private

Function 'createItem' could be private

Function 'createInfoObjectModel' could be private

Property 'SEPARATOR' could be private

Property 'point' could be private

Function 'configureToolbar' could be private

Property 'resetActions' could be private

Property 'defaultZoomLevel' could be private

Function 'showHint' could be private

Property 'leanInfoviewService' could be private

Function 'createDocPanel' could be private

Implicit parameter 'it' of enclosing lambda is shadowed

Implicit parameter 'it' of enclosing lambda is shadowed

Implicit parameter 'it' of enclosing lambda is shadowed

Implicit parameter 'it' of enclosing lambda is shadowed

Private property name `SLEEP_TIME` should not contain underscores in the middle or the end

Private property name `BORDER` should not start with an uppercase letter

Property name `VALUE_KEYS` should start with a lowercase letter

Property name `KEY_KEYS` should start with a lowercase letter

Property name `KEYWORD_IN_PROOF` should start with a lowercase letter

Property name `SORRY_KEYS` should start with a lowercase letter

Property name `KEY` should start with a lowercase letter

Property name `KEYWORD_IN_PROOF_KEYS` should start with a lowercase letter

Property name `NUMBER_KEYS` should start with a lowercase letter

Property name `EMPTY_KEYS` should start with a lowercase letter

Property name `VALUE` should start with a lowercase letter

Property name `COMMENT` should start with a lowercase letter

Property name `SORRY` should start with a lowercase letter

Property name `SEPARATOR` should start with a lowercase letter

Property name `SEPARATOR_KEYS` should start with a lowercase letter

Property name `NUMBER` should start with a lowercase letter

Property name `COMMENT_KEYS` should start with a lowercase letter

Property name `BAD_CHAR_KEYS` should start with a lowercase letter

Redundant 'if' statement

Redundant 'if' statement

Redundant curly braces in string template

Redundant curly braces in string template

Redundant empty class body

Remove explicit type arguments

Replace negated 'isEmpty' with 'isNotEmpty'

Replace negated 'isEmpty' with 'isNotEmpty'

The opt-in annotation is redundant: no matching experimental API is used

The opt-in annotation is redundant: no matching experimental API is used

The opt-in annotation is redundant: no matching experimental API is used

Use of getter method instead of property access syntax

Use of setter method instead of property access syntax

Use of setter method instead of property access syntax

Use of getter method instead of property access syntax

Use of getter method instead of property access syntax