Skip to content

Commit

Permalink
feat: add subtle spinner while infoview is loading (#546)
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi authored Nov 8, 2024
1 parent be04ab3 commit 1e4804f
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 2 deletions.
2 changes: 1 addition & 1 deletion lean4-infoview/package.json
Original file line number Diff line number Diff line change
@@ -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",
Expand Down
21 changes: 21 additions & 0 deletions lean4-infoview/src/infoview/info.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -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: 'calc(0.8 * var(--vscode-font-size))',
}

return (
<summary style={{ transition: 'color 0.5s ease' }} className={'mv2 pointer ' + statusColor}>
{locationString}
{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>
<span
className="fr"
onClick={e => {
Expand Down
2 changes: 1 addition & 1 deletion package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit 1e4804f

Please sign in to comment.