diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json index 4ae23636..7cc04602 100644 --- a/lean4-infoview/package.json +++ b/lean4-infoview/package.json @@ -1,6 +1,6 @@ { "name": "@leanprover/infoview", - "version": "0.7.8", + "version": "0.7.9", "description": "An interactive display for the Lean 4 theorem prover.", "scripts": { "watch": "rollup --config --environment NODE_ENV:development --watch", diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index f13bb670..c8a423ae 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/lean4-infoview/src/infoview/info.tsx @@ -63,12 +63,33 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { const locationString = `${basename(pos.uri)}:${pos.line + 1}:${pos.character}` const isPinned = kind === 'pin' + const spinnerStyle: React.CSSProperties = { + opacity: status === 'updating' ? 1 : 0, + animationName: 'spin', + animationIterationCount: 'infinite', + transitionDuration: '0.15s', + transitionProperty: 'opacity', + transitionTimingFunction: 'ease-in', + color: 'var(--vscode-editor-foreground)', + fontSize: '10px', + } + return ( {locationString} {isPinned && !isPaused && ' (pinned)'} {!isPinned && isPaused && ' (paused)'} {isPinned && isPaused && ' (pinned and paused)'} + + + { diff --git a/package-lock.json b/package-lock.json index 052cc5a2..3e8ff2ee 100644 --- a/package-lock.json +++ b/package-lock.json @@ -28,7 +28,7 @@ }, "lean4-infoview": { "name": "@leanprover/infoview", - "version": "0.7.8", + "version": "0.7.9", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview-api": "~0.4.0",