feat: add a setting to disable the loading spinner animation

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 =

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)'}
-            <span style={spinnerStyle} className="mh2 codicon codicon-loading" title="updating">
-                <style>
-                    {`
-                        @keyframes spin {
-                            0% { transform: rotate(0deg); }
-                            100% { transform: rotate(360deg); }
-                        }
-                    `}
-                </style>
-            </span>
+            {!config.disableLoadingSpinner && (
+                <span style={spinnerStyle} className="mh2 codicon codicon-loading" title="updating">
+                    <style>
+                        {`
+                            @keyframes spin {
+                                0% { transform: rotate(0deg); }
+                                100% { transform: rotate(360deg); }
+                            }
+                        `}
+                    </style>
+                </span>
+            )}
+
             <span
                 className="fr"
                 onClick={e => {

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,

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)
 }

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(),
         })
     }