From 1e4804fcf93f02c77e10dea4ef389af4e78d8e31 Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Fri, 8 Nov 2024 13:31:52 +0100
Subject: [PATCH] feat: add subtle spinner while infoview is loading (#546)

![Recording 2024-11-06 at 14 52
53](https://github.com/user-attachments/assets/1793d1a2-57db-409f-ae66-71a648ea8300)

Closes #470.
---
 lean4-infoview/package.json          |  2 +-
 lean4-infoview/src/infoview/info.tsx | 21 +++++++++++++++++++++
 package-lock.json                    |  2 +-
 3 files changed, 23 insertions(+), 2 deletions(-)

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..7bcd0f32 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: '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 => {
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",