feat: editor decorations (#585)

This PR adds several new editor decorations.

### Error and warning gutter decorations

To resolve the issue that warnings and errors can sometimes be a bit
difficult to spot, especially when the corresponding diagnostic squiggly
is small, this PR adds a system of gutter decorations to make errors and
warnings much more visible.

![Error and warning gutter
decorations](https://github.com/user-attachments/assets/a611e2ea-aa26-4c1f-b945-8e86dfbeef4c)

The circled error and warning symbols denote the line where an error or
a warning starts, i.e. where the squiggly is displayed. A red vertical
line denotes the *full range* of the error, i.e. the range in which the
error is displayed under 'Messages' in the InfoView. The red line bends
to the right whenever a full error range ends in that line of code.
Single line errors are displayed without a red line.

These gutter decorations can be disabled using the 'Lean4: Show
Diagnostic Gutter Decorations' setting. When the gutter icons of the
Error Lens extension are enabled, the gutter decorations of the Lean 4
VS Code extension are disabled.

Once this PR is merged, this feature will be available in all Lean 4
versions.

### 'Unsolved goals' markers

To resolve the issue that it can sometimes be a bit difficult to tell
where one should continue typing in a proof, this PR adds an end-of-line
editor decoration that is displayed in the line where the full range of
an 'unsolved goals' error ends.

![Unsolved goals
markers](https://github.com/user-attachments/assets/32562122-6ce6-490e-a9db-5ae3e8a6e79f)

The 'unsolved goals' markers can be disabled using the 'Lean 4: Show
Unsolved Goal Decoration' setting.

This feature needs language server support, so it will only be active
for Lean versions that include the companion PR at
leanprover/lean4#7366.

### Goals accomplished!

To re-introduce some positive reinforcement into Lean 4 after the 'Goals
accomplished!' message from Lean 3 was removed due to often being
confusing in Lean 4, this PR adds a new 'Goals accomplished!' mechanism
when a theorem or a `Prop`-typed `example` has been proven.

![Goals
accomplished](https://github.com/user-attachments/assets/f303d580-cd4a-4697-80e6-d0d1114fd454)

When a theorem or a `Prop`-typed `example` contains no errors or
`sorry`s anymore, two blue checkmarks appear next to the start of the
declaration as a gutter decoration. Additionally, a 'Goals
accomplished!' message appears under 'Messages' in the InfoView. The
'Goals accomplished!' message does not appear in 'All Messages' and is
not displayed with a squiggly line in the editor.

The 'Goals accomplished!' gutter decoration can be configured or
disabled using the 'Lean 4: Goals Accomplished Decoration Kind' setting.
In addition to the default double checkmark decoration pictured above,
this PR adds the following additional styles for the gutter decoration:

- Circled checkmark:

![Circled
checkmark](https://github.com/user-attachments/assets/0014bf2c-6dee-4af7-9c01-7cd470efa1ca)

- Octopus:


![Octopus](https://github.com/user-attachments/assets/9a65ad3b-d032-414c-b632-3afc943d45ae)

- Tada:


![Tada](https://github.com/user-attachments/assets/942e3973-444c-4701-b86a-0570ff437cd0)

This feature needs language server support, so it will only be active
for Lean versions that include the companion PR at
leanprover/lean4#7366.

### Technical notes
- We intend to test this implementation for the 'unsolved goals' markers
and 'Goals accomplished!' in core before v4.19.0-rc1 to iron out any
remaining issues.
- All gutter decorations are implemented using .svgs, which is the only
API that VS Code provides to display things in the gutter. Since there
are lots of different cases to consider for the red vertical error range
lines, as well as for light and dark themes, this PR ships 56 .svg files
in total.
- The design language of the red lines for the error range gutter
decorations is deliberately not perfectly unambiguous. For example, when
multiple full error ranges overlap, it isn't clear which error range is
terminated by the line bending to the right. The design in this PR is
the best I could come up with for the limited size of the gutter without
introducing too much visual complexity or noise.
- The task gutter had to be rewritten entirely for this PR, including
the progress bar code.
- Since the line where the full range of an 'unsolved goals' error ends
is relatively unstable as the document is being edited, this PR
implements an edit delay of 3000ms for 'unsolved goals' markers, so that
they do not constantly jump around while editing the document.
- The 'unsolved goals' markers use an emoji (specifically the 'Hammer
and wrench' emoji U+1F6E0) instead of an icon. The reason for this is
that VS Code's decoration API appears to be pretty broken for
end-of-line icons and fails to vertically center them correctly.
- None of these decorations have an associated hover to explain the
semantics of each decoration. The reason for this is that VS Code
doesn't support gutter decoration hovers and for end-of-line
decorations, it pollutes the hover of every hover in the whole line with
the hover message of the end-of-line decoration.
- This PR includes the client-side for the protocol extensions defined
at leanprover/lean4#7366.

Author: mhuisi

lean4-infoview-api/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.5.0",
+    "version": "0.6.0",
     "description": "Types and API for @leanprover/infoview.",
     "scripts": {
         "watch": "tsc --watch",

lean4-infoview-api/src/lspTypes.ts

@@ -1,16 +1,30 @@
 import type {
     Diagnostic,
     DocumentUri,
+    integer,
     Range,
     TextDocumentPositionParams,
     VersionedTextDocumentIdentifier,
 } from 'vscode-languageserver-protocol'
 
 // Lean 4 extensions to LSP.
 
+export enum LeanTag {
+    UnsolvedGoals = 1, // introduced in 2025-03-05
+    GoalsAccomplished = 2, // introduced in 2025-03-05
+}
+
 /** Used in place of {@link Diagnostic} within `textDocument/publishDiagnostics`. */
 export interface LeanDiagnostic extends Diagnostic {
     fullRange?: Range // introduced in 2021-03-10
+    isSilent?: boolean // introduced in 2025-03-05
+    leanTags?: LeanTag[] // introduced in 2025-03-05
+}
+
+export interface LeanPublishDiagnosticsParams {
+    uri: DocumentUri
+    version?: integer
+    diagnostics: LeanDiagnostic[]
 }
 
 export interface PlainGoal {

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.8.2",
+    "version": "0.8.3",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -49,7 +49,7 @@
         "typescript": "^5.4.5"
     },
     "dependencies": {
-        "@leanprover/infoview-api": "~0.5.0",
+        "@leanprover/infoview-api": "~0.6.0",
         "@vscode/codicons": "^0.0.32",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",

lean4-infoview/src/infoview/contexts.ts

@@ -1,7 +1,12 @@
 import * as React from 'react'
-import type { Diagnostic, DocumentUri } from 'vscode-languageserver-protocol'
+import type { DocumentUri } from 'vscode-languageserver-protocol'
 
-import { defaultInfoviewConfig, InfoviewConfig, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'
+import {
+    defaultInfoviewConfig,
+    InfoviewConfig,
+    LeanDiagnostic,
+    LeanFileProgressProcessingInfo,
+} from '@leanprover/infoview-api'
 
 import { EditorConnection } from './editorConnection'
 import { ServerVersion } from './serverVersion'
@@ -13,7 +18,7 @@ export const EditorContext = React.createContext<EditorConnection>(null as any)
 export const VersionContext = React.createContext<ServerVersion | undefined>(undefined)
 
 export const ConfigContext = React.createContext<InfoviewConfig>(defaultInfoviewConfig)
-export const LspDiagnosticsContext = React.createContext<Map<DocumentUri, Diagnostic[]>>(new Map())
+export const LspDiagnosticsContext = React.createContext<Map<DocumentUri, LeanDiagnostic[]>>(new Map())
 export const ProgressContext = React.createContext<Map<DocumentUri, LeanFileProgressProcessingInfo[]>>(new Map())
 
 /**

lean4-infoview/src/infoview/info.tsx

@@ -1,5 +1,5 @@
 import * as React from 'react'
-import type { Diagnostic, Location } from 'vscode-languageserver-protocol'
+import type { Location } from 'vscode-languageserver-protocol'
 
 import {
     getInteractiveDiagnostics,
@@ -415,13 +415,13 @@ function InfoAux(props: InfoProps) {
     // Compute the LSP diagnostics at this info's position. We try to ensure that if these remain
     // the same, then so does the identity of `lspDiagsHere` so that it can be used as a dep.
     const lspDiags = React.useContext(LspDiagnosticsContext)
-    const [lspDiagsHere, setLspDiagsHere] = React.useState<Diagnostic[]>([])
+    const [lspDiagsHere, setLspDiagsHere] = React.useState<LeanDiagnostic[]>([])
     React.useEffect(() => {
         // Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b
         setLspDiagsHere(diags0 => {
-            const diagPred = (d: Diagnostic) =>
+            const diagPred = (d: LeanDiagnostic) =>
                 RangeHelpers.contains(
-                    (d as LeanDiagnostic).fullRange || d.range,
+                    d.fullRange || d.range,
                     { line: pos.line, character: pos.character },
                     config.allErrorsOnLine,
                 )

lean4-infoview/src/infoview/messages.tsx

@@ -1,14 +1,8 @@
 import * as React from 'react'
 import fastIsEqual from 'react-fast-compare'
-import {
-    Diagnostic,
-    DiagnosticSeverity,
-    DocumentUri,
-    Location,
-    PublishDiagnosticsParams,
-} from 'vscode-languageserver-protocol'
+import { Diagnostic, DiagnosticSeverity, DocumentUri, Location } from 'vscode-languageserver-protocol'
 
-import { LeanDiagnostic, RpcErrorCode } from '@leanprover/infoview-api'
+import { LeanDiagnostic, LeanPublishDiagnosticsParams, RpcErrorCode } from '@leanprover/infoview-api'
 
 import { getInteractiveDiagnostics, InteractiveDiagnostic } from '@leanprover/infoview-api'
 import { Details } from './collapsing'
@@ -135,7 +129,9 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
     const rs0 = useRpcSessionAtPos({ uri: uri0, line: 0, character: 0 })
     const dc = React.useContext(LspDiagnosticsContext)
     const config = React.useContext(ConfigContext)
-    const diags0 = React.useMemo(() => dc.get(uri0) || [], [dc, uri0])
+    const diags0 = React.useMemo(() => dc.get(uri0) || [], [dc, uri0]).filter(
+        diag => diag.isSilent === undefined || !diag.isSilent,
+    )
 
     const iDiags0 = React.useMemo(
         () =>
@@ -145,7 +141,8 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
                 // ensures that the call doesn't block until the whole file is elaborated.
                 const maxLine = diags0.reduce((ln, d) => Math.max(ln, d.range.end.line), 0) + 1
                 try {
-                    const diags = await getInteractiveDiagnostics(rs0, { start: 0, end: maxLine })
+                    let diags = await getInteractiveDiagnostics(rs0, { start: 0, end: maxLine })
+                    diags = diags.filter(d => d.isSilent === undefined || !d.isSilent)
                     if (diags.length > 0) {
                         return diags
                     }
@@ -159,7 +156,7 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
                         console.log('getInteractiveDiagnostics error ', err)
                     }
                 }
-                return diags0.map(d => ({ ...(d as LeanDiagnostic), message: { text: d.message } }))
+                return diags0.map(d => ({ ...d, message: { text: d.message } }))
             }),
         [rs0, diags0],
     )
@@ -247,8 +244,8 @@ function AllMessagesBody({ uri, messages, setNumDiags }: AllMessagesBodyProps) {
 export function WithLspDiagnosticsContext({ children }: React.PropsWithChildren<{}>) {
     const [allDiags, _0] = useServerNotificationState(
         'textDocument/publishDiagnostics',
-        new Map<DocumentUri, Diagnostic[]>(),
-        async (params: PublishDiagnosticsParams) => diags => new Map(diags).set(params.uri, params.diagnostics),
+        new Map<DocumentUri, LeanDiagnostic[]>(),
+        async (params: LeanPublishDiagnosticsParams) => diags => new Map(diags).set(params.uri, params.diagnostics),
         [],
     )