Merge branch 'master' into indent-focus-block-rule

.eslintrc.js

@@ -61,7 +61,7 @@ module.exports = {
         "@typescript-eslint/no-explicit-any": "off",
         "@typescript-eslint/no-misused-new": "error",
         "@typescript-eslint/no-unused-vars": "off",
-        "@typescript-eslint/no-namespace": "error",
+        "@typescript-eslint/no-namespace": "off",
         "@typescript-eslint/no-parameter-properties": "off",
         "@typescript-eslint/no-inferrable-types": "off",
         "@typescript-eslint/no-use-before-define": "off",

.github/workflows/on-push.yml

@@ -43,7 +43,14 @@ jobs:
           npm ci
           npx lerna bootstrap --ci
           npm run build
-          npx lerna run --scope=lean4 package
+
+      - name: Package
+        run: npx lerna run --scope=lean4 package
+        if: ${{ !startsWith(github.ref, 'refs/tags/v') || !endsWith(github.ref, '-pre') }}
+
+      - name: Package pre-release
+        run: npx lerna run --scope=lean4 packagePreRelease
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && endsWith(github.ref, '-pre') }}
 
       - name: Upload artifact
         uses: actions/upload-artifact@v2
@@ -53,21 +60,32 @@ jobs:
           path: 'vscode-lean4/lean4-*.vsix'
 
       - name: Publish packaged extension
-        if: startsWith(github.ref, 'refs/tags/v') && matrix.os == 'ubuntu-latest'
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
         run: |
           cd vscode-lean4
-          npx vsce publish -i lean4-*.vsix
+          npx @vscode/vsce publish -i lean4-*.vsix
           npx ovsx publish lean4-*.vsix
         env:
           OVSX_PAT: ${{ secrets.OVSX_PAT }}
           VSCE_PAT: ${{ secrets.VSCE_PAT }}
 
+      - name: Publish packaged pre-release extension
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
+        run: |
+          cd vscode-lean4
+          npx @vscode/vsce publish --pre-release -i lean4-*.vsix
+          npx ovsx publish --pre-release lean4-*.vsix
+        env:
+          OVSX_PAT: ${{ secrets.OVSX_PAT }}
+          VSCE_PAT: ${{ secrets.VSCE_PAT }}
+
       - name: Upload extension as release
         if: startsWith(github.ref, 'refs/tags/v') && matrix.os == 'ubuntu-latest'
         uses: softprops/action-gh-release@v1
         with:
           files: 'vscode-lean4/lean4-*.vsix'
           fail_on_unmatched_files: true
+          prerelease: ${{ endsWith(github.ref, '-pre') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 

.vscode/settings.json

@@ -8,5 +8,8 @@
     },
     "typescript.tsdk": "./node_modules/typescript/lib", // we want to use the TS server from our node_modules folder to control its version
     "files.insertFinalNewline": true,
-    "files.trimTrailingWhitespace": true
+    "files.trimTrailingWhitespace": true,
+    "[markdown]": {
+        "files.trimTrailingWhitespace": false
+    }
 }

README.md

@@ -19,9 +19,9 @@ containing the following:
 1. Open your file `hello.lean`.
 1. If `Lean` is not yet installed on your system you will see a prompt like this:
 
-    ![prompt](vscode-lean4/media/install-elan.png)
+    ![prompt](vscode-lean4/media/install-lean.png)
 
-1. Click the `Install Lean using Elan` option and enter any default options that appear in the terminal window.
+1. Click the `Install Lean` option and enter any default options that appear in the terminal window.
 1. After this succeeds the correct version of Lean will be installed by `elan`
 and you should see something like this in the `Lean: Editor` output panel:
     ```
@@ -136,8 +136,8 @@ You can also disable auto-opening behavior using the setting `lean4.infoViewAuto
   | Symbol | Description |
   |--------|-------------|
   | ![quotes](vscode-lean4/media/quotes.png) | Copy the contents of the widget to a comment in the active text editor. |
-  | ![pin](vscode-lean4/media/pin.png) | Split off a "pinned" tactic state widget, which tracks the tactic state at a fixed position, even if you move your cursor away.  When pinned you will see the unpin and reveal file location icons appear. |
-  | ![unpin](vscode-lean4/media/unpin.png) | Remove a pinned widget from the Infoview. |
+  | ![pin](vscode-lean4/media/pin.png) | Remove a pinned widget from the Infoview. |
+  | ![unpin](vscode-lean4/media/unpin.png) | Split off a "pinned" tactic state widget, which tracks the tactic state at a fixed position, even if you move your cursor away.  When pinned you will see the unpin and reveal file location icons appear. |
   | ![reveal](vscode-lean4/media/reveal-file-location.png) | Move the cursor in the editor to the pinned location in the file. |
   | ![pause](vscode-lean4/media/pause.png) | Prevent the tactic state widget from updating when the file is edited. When paused you will see the following addition icons show up.
   | ![continue](vscode-lean4/media/continue.png) | Once paused you can then click this icon to resume updates. |
@@ -191,6 +191,8 @@ name of the relative path to the store the logs.
 
 * `lean4.typesInCompletionList`: controls whether the types of all items in the list of completions are displayed. By default, only the type of the highlighted item is shown.
 
+* `lean4.fallBackToStringOccurrenceHighlighting`: controls whether the editor should fall back to string-based occurrence highlighting when there are no symbol occurrences found.
+
 ### Infoview settings
 
 * `lean4.infoview.autoOpen`: controls whether the Infoview is automatically displayed when the Lean extension is activated for the first time in a given VS Code workspace(`true` by default).  If you manually close the Infoview it will stay closed for that workspace until.  You can then open it again using the <kbd>Ctrl</kbd>+<kbd>Shift</kbd>+<kbd>P</kbd> `Lean 4: Infoview: Display Goal` command.
@@ -209,6 +211,18 @@ name of the relative path to the store the logs.
 
 * `lean4.infoview.reverseTacticState`: show each goal above its local context by default. This can also be toggled by clicking a button (see the Infoview panel description above). The default is `false`.
 
+#### Colors
+
+These colors are used to display proof states in the infoview:
+
+* `lean4.infoView.hypothesisName`: accessible hypothesis names
+* `lean4.infoView.inaccessibleHypothesisName`: inaccessible hypothesis names
+* `lean4.infoView.goalCount`: the number of goals
+* `lean4.infoView.turnstile`: the turnstile (⊢) that separates the hypotheses from the goal
+* `lean4.infoView.caseLabel`: case labels (e.g. `case zero`)
+
+They can be set in a color theme, or under `workbench.colorCustomizations` in the settings file.
+
 ## Extension commands
 
 This extension also contributes the following commands, which can be bound to keys if desired using the [VS Code keyboard bindings](https://code.visualstudio.com/docs/getstarted/keybindings).

docs/bootstrapping.md

@@ -16,7 +16,7 @@ yet and in that case `getLeanVersion` calls `testLeanVersion` on the
 
 ![prompt](images/InstallPrompt.png)
 
-If the user clicks `Install Lean using Elan` then this will happen
+If the user clicks `Install Lean` then this will happen
 and elan will be installed in the default location and a stable build
 of Lean will also be installed.
 

docs/dev.md

@@ -14,7 +14,7 @@ See the following design topics:
 
 ### Building
 - Make sure you have an up to date installation of `npm` and `node.js`.  For example `npm` version 8.1.3 and `node.js` version v16.13.0.
-- Run `npm install` in this folder. This installs the Lerna package manager.
+- Run `npm install` in your workspace root folder. This installs the Lerna package manager.
 - Run `npx lerna bootstrap`. This sets up the project's dependencies.
 - Run `npx lerna run build`. This compiles the extension (which is necessary for go-to-definition in VS Code).
 

docs/language-configuration.md

@@ -24,3 +24,25 @@ This rule ensures that hitting enter after starting a focus block during a tacti
   · intro x| <-- hit enter here
     | <-- cursor ends up here
 ```
+
+## [`brackets`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#brackets-definition), [`autoClosingPairs`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#autoclosing), and [`surroundingPairs`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#autosurrounding)
+
+All of these fields handle brackets in different ways.
+
+* `brackets`: determines highlighting and selection
+* `autoClosingPairs`: specifies which bracket pairs should prompt automatic insertion of a closing bracket upon typing the initial bracket
+* `surroundingPairs`: specifies which brackets should surround highlighted content when typed (e.g. highlighting a term then typing <kbd>(</kbd> should surround the term with parentheses)
+
+### Markdown
+
+We include the following only in `surroundingPairs`:
+
+```json
+    ...
+    ["`", "`"],
+    ["*", "*"],
+    ["_", "_"]
+    ...
+```
+
+This means that you can highlight text in comments and italicize, bold, or code-format it easily by typing the respective marker(s). We don't want to use these as actual brackets or autoclosing pairs, however, due to their use in Lean code.

lean4-infoview-api/src/rpcApi.ts

@@ -153,8 +153,9 @@ export function getGoToLocation(rs: RpcSessionAtPos, kind: GoToKind, info: InfoW
 
 export interface UserWidget {
     id: string;
-    /** Pretty user name. */
-    name: string;
+    /** Newer widget APIs do not send this.
+     * In previous versions, it used to be a user-readable name to show in a title bar. */
+    name?: string;
     /** A hash (provided by Lean) of the widgetSource's sourcetext.
      * This is used to look up the WidgetSource object.
      */

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@leanprover/infoview",
-  "version": "0.4.3",
+  "version": "0.4.5",
   "description": "An interactive display for the Lean 4 theorem prover.",
   "scripts": {
     "watch": "rollup --config --environment NODE_ENV:development --watch",

lean4-infoview/src/index.tsx

@@ -12,7 +12,7 @@ export { EditorContext, VersionContext } from './infoview/contexts';
 export { EditorConnection } from './infoview/editorConnection';
 export { RpcContext } from './infoview/rpcSessions';
 export { ServerVersion } from './infoview/serverVersion';
-export { GoalLocation, GoalsLocation } from './infoview/goalLocation';
+export { LocationsContext, GoalLocation, GoalsLocation } from './infoview/goalLocation';
 export { importWidgetModule, DynamicComponent, DynamicComponentProps,
     PanelWidgetProps } from './infoview/userWidget';
 

lean4-infoview/src/infoview/index.css

@@ -30,27 +30,17 @@ html,body {
 }
 
 /* These are syntax highlights for the string goal view. */
-.goal-goals { color: #569cd6; }
-.goal-vdash { color: #569cd6; }
-.goal-case { color: #a1df90; }
-.goal-hyp { color: #ffcc00; }
+.goal-goals { color: var(--vscode-lean4-infoView\.goalCount); }
+.goal-vdash { color: var(--vscode-lean4-infoView\.turnstile); }
+.goal-case { color: var(--vscode-lean4-infoView\.caseLabel); }
+.goal-hyp { color: var(--vscode-lean4-infoView\.hypothesisName); }
 .goal-inaccessible {
-    color: var(--vscode-editor-foreground);
+    color: var(--vscode-lean4-infoView\.inaccessibleHypothesisName);
     opacity: 0.7;
     font-style: italic;
     font-weight: normal;
 }
 
-.vscode-light .goal-goals { color: #367cb6; }
-.vscode-light .goal-vdash { color: #367cb6; }
-.vscode-light .goal-case { color: #1f7a1f; }
-.vscode-light .goal-hyp { color: #cc7a00; }
-
-.vscode-high-contrast  .goal-goals { color: var(--vscode-terminal-ansiBlue); }
-.vscode-high-contrast  .goal-vdash { color: var(--vscode-terminal-ansiBlue); }
-.vscode-high-contrast  .goal-case { color: var(--vscode-terminal-ansiGreen); }
-.vscode-high-contrast  .goal-hyp { color: var(--vscode-terminal-ansiYellow); }
-
 /* Used to denote text highlighted by the pretty-print expression widget. */
 .highlightable {
     border-radius: 2pt;

lean4-infoview/src/infoview/info.tsx

@@ -8,7 +8,7 @@ import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext }
 import { lspDiagToInteractive, MessagesList } from './messages';
 import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic,
     InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
-    RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
+    RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal, LeanDiagnostic } from '@leanprover/infoview-api';
 import { PanelWidgetDisplay } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
 import { GoalsLocation, Locations, LocationsContext } from './goalLocation';
@@ -130,13 +130,22 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             initiallyOpen={config.showExpectedType}
             displayCount={false}
             togglingAction='toggleExpectedType' />
-        {userWidgets.map(widget =>
-            <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
-                <summary className='mv2 pointer'>{widget.name}</summary>
-                <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []} termGoal={termGoal}
-                    selectedLocations={selectedLocs} widget={widget}/>
-            </details>
-        )}
+        {userWidgets.map(widget => {
+            const inner =
+                <PanelWidgetDisplay key={`widget::${widget.id}::${widget.range?.toString()}`}
+                    pos={pos}
+                    goals={goals ? goals.goals : []}
+                    termGoal={termGoal}
+                    selectedLocations={selectedLocs}
+                    widget={widget} />
+            if (widget.name)
+                return <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
+                    <summary className='mv2 pointer'>{widget.name}</summary>
+                    {inner}
+                </details>
+            else
+                return inner
+        })}
         <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
             <details key='messages' open>
                 <summary className='mv2 pointer'>Messages ({messages.length})</summary>
@@ -258,7 +267,7 @@ function InfoAux(props: InfoProps) {
         // 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) =>
-                RangeHelpers.contains(d.range, {line: pos.line, character: pos.character}, config.allErrorsOnLine)
+                RangeHelpers.contains((d as LeanDiagnostic).fullRange || d.range, {line: pos.line, character: pos.character}, config.allErrorsOnLine)
             const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred)
             if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0
             return newDiags