diff --git a/lean4-infoview-api/src/infoviewApi.ts b/lean4-infoview-api/src/infoviewApi.ts
index abc79ded8..fdc218737 100644
--- a/lean4-infoview-api/src/infoviewApi.ts
+++ b/lean4-infoview-api/src/infoviewApi.ts
@@ -86,6 +86,7 @@ export interface InfoviewConfig {
emphasizeFirstGoal: boolean
reverseTacticState: boolean
showTooltipOnHover: boolean
+ disableLoadingSpinner: boolean
}
export const defaultInfoviewConfig: InfoviewConfig = {
@@ -97,6 +98,7 @@ export const defaultInfoviewConfig: InfoviewConfig = {
emphasizeFirstGoal: false,
reverseTacticState: false,
showTooltipOnHover: true,
+ disableLoadingSpinner: false,
}
export type InfoviewActionKind =
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index 7bcd0f326..8d12673dc 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -50,6 +50,7 @@ interface InfoStatusBarProps extends InfoPinnable, PausableProps {
}
const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
+ const config = React.useContext(ConfigContext)
const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props
const ec = React.useContext(EditorContext)
@@ -80,16 +81,19 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
{isPinned && !isPaused && ' (pinned)'}
{!isPinned && isPaused && ' (paused)'}
{isPinned && isPaused && ' (pinned and paused)'}
-
-
-
+ {!config.disableLoadingSpinner && (
+
+
+
+ )}
+
{
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
index a95eae3f9..addc44b9f 100644
--- a/vscode-lean4/package.json
+++ b/vscode-lean4/package.json
@@ -156,6 +156,11 @@
"default": true,
"markdownDescription": "Show the tooltip for an interactive element (e.g. a subexpression) when the pointer hovers over that element. When disabled, the element must be clicked for the tooltip to show up."
},
+ "lean4.infoview.disableLoadingSpinner": {
+ "type": "boolean",
+ "default": false,
+ "markdownDescription": "Disable the loading spinner on the infoview."
+ },
"lean4.elaborationDelay": {
"type": "number",
"default": 200,
diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts
index 94a71a2a4..c30c045ad 100644
--- a/vscode-lean4/src/config.ts
+++ b/vscode-lean4/src/config.ts
@@ -82,6 +82,10 @@ export function getInfoViewShowTooltipOnHover(): boolean {
return workspace.getConfiguration('lean4.infoview').get('showTooltipOnHover', true)
}
+export function getInfoViewDisableLoadingSpinner(): boolean {
+ return workspace.getConfiguration('lean4.infoview').get('disableLoadingSpinner', false)
+}
+
export function getElaborationDelay(): number {
return workspace.getConfiguration('lean4').get('elaborationDelay', 200)
}
diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts
index 3412ced88..ff4c0d51b 100644
--- a/vscode-lean4/src/infoview.ts
+++ b/vscode-lean4/src/infoview.ts
@@ -34,6 +34,7 @@ import {
getInfoViewAutoOpen,
getInfoViewAutoOpenShowsGoal,
getInfoViewDebounceTime,
+ getInfoViewDisableLoadingSpinner,
getInfoViewEmphasizeFirstGoal,
getInfoViewReverseTacticState,
getInfoViewShowExpectedType,
@@ -664,6 +665,7 @@ export class InfoProvider implements Disposable {
emphasizeFirstGoal: getInfoViewEmphasizeFirstGoal(),
reverseTacticState: getInfoViewReverseTacticState(),
showTooltipOnHover: getInfoViewShowTooltipOnHover(),
+ disableLoadingSpinner: getInfoViewDisableLoadingSpinner(),
})
}