add commit tooltips to project info

Projects/mathlib-demo/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a975dea2c4d8258a55b4f9861c537e2bb0f9ef63",
+   "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5f2879ac9e132974c6e229f6139d2d0ab2fdd4dd",
+   "rev": "9b07fb6d08b58de5b55813b29f5ac9aa6fa0b1ad",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

client/src/Popups/Tools.tsx

@@ -1,5 +1,5 @@
 import { Popup } from '../Navigation'
-import { FC, useEffect, useState } from 'react'
+import { FC, useEffect, useRef, useState } from 'react'
 
 // TODO: Do these interfaces exist somewhere in vscode-lean4?
 // They might need to be updated manually if changes to `lake` occur.
@@ -42,6 +42,94 @@ const emptyManifest: LakeManifest = {
   lakeDir: ""
 }
 
+/** These are just a few relevant fields the data fetched from github comprises. */
+interface CommitInfo {
+  sha: string,
+  commit: {
+    author: {
+      name: string,
+      date: string
+    },
+    message: string
+  },
+  author: {
+    avatar_url: string
+  },
+  stats: {
+    total: number,
+    additions: number,
+    deletions: number,
+  }
+}
+
+/** Displays a link of the specified commit together with a hover-tooltip showing the
+ * information from github.
+ *
+ * Note that github has a rate limit (60 requests/h), but since this should be a
+ * rarely used feature, it might be fine for now.
+ */
+const ToolTip: FC<{
+  pkg: LakePackage
+}> = ({pkg}) => {
+  const [loaded, setLoaded] = useState(false)
+  const linkRef = useRef<HTMLAnchorElement>(null)
+  const [commit, setCommit] = useState<CommitInfo>()
+  const [error, setError] = useState<string>()
+
+  useEffect(() => {
+    linkRef.current?.addEventListener('mouseover', handleHover)
+    return () => {
+      linkRef.current?.removeEventListener('mouseover', handleHover)
+    }
+  }, [linkRef, loaded])
+
+  // Load commit info on hovering the first time
+  const handleHover = (_event: any) => {
+    // Do not fetch twice
+    if (loaded) { return }
+    setLoaded(true)
+
+    // Hack: construct github api URL from repo URL
+    let githubUrl = pkg.url.replace('github.com/', 'api.github.com/repos/') + `/commits/${pkg.rev}`
+    console.debug(`[LeanWeb]: fetch from ${githubUrl}`)
+
+    fetch(githubUrl).then(response => {
+      if (! response.ok) {
+        console.warn(`[LeanWeb]: failed request (${response.status})`, response)
+      }
+      return response.json()
+    }).then(data => {
+      if (data.message) {
+        // e.g. when reaching rate limit
+        setError(data.message)
+      } else {
+        setCommit(data)
+      }
+    }).catch(error => {
+      setError(error)
+      console.error(error)
+    })
+  }
+
+  return <a ref={linkRef} className="tooltip" href={`${pkg.url}/commits/${pkg.rev}/`} target='_blank' >{pkg.rev.substring(0,7)}
+  <div className="tooltiptext" id="tooltip-content">
+    { error ?
+        <p>{error}</p> :
+      (loaded && commit) ? <>
+        {/* valid */}
+        <img src={commit?.author?.avatar_url} />
+        <p>
+          <span className="commit-date">{new Date(commit?.commit?.author?.date).toLocaleString()}</span><br/>
+          <span className="commit-message">{commit?.commit?.message.split('\n')[0]}</span> <span className="commit-author">by {commit?.commit?.author?.name}</span><br/>
+          <span className="commit-sha">{commit?.sha}</span>
+        </p>
+      </> : <p>Loading…</p>
+    }
+  </div>
+</a>
+}
+
+/** Shows important information about the Lean project loaded in the web editor */
 const ToolsPopup: FC<{
   open: boolean
   project: string
@@ -114,7 +202,7 @@ const ToolsPopup: FC<{
             <td>{pkg.name}</td>
             { pkg.type == 'git' ?
               <>
-                <td><a href={`${pkg.url}/commits/${pkg.rev}/`} target='_blank' >{pkg.rev.substring(0,7)}</a></td>
+                <td><ToolTip pkg={pkg} /></td>
                 <td>{pkg.inputRev}</td>
               </> : <td colSpan={2}>(local package)</td>
             }

client/src/css/Editor.css

@@ -97,6 +97,7 @@
 code {
   font-family: 'Source Code Pro', 'STIX Two Math', monospace;
   color: var(--vscode-textPreformat-foreground);
+  background-color: var(--vscode-textPreformat-background);
 }
 
 

client/src/css/Navigation.css

@@ -90,4 +90,63 @@ nav .nav-link:hover {
 nav select {
   margin-left: .5rem;
   margin-right: .5rem;
-}
+}
+
+.tooltip {
+  position: relative;
+  cursor: pointer;
+}
+
+.tooltip .tooltiptext {
+  visibility: hidden;
+  min-width: 300px;
+  background-color: var(--vscode-input-foreground);
+  color: var(--vscode-input-background);
+  text-align: left;
+  border-radius: 5px;
+  padding: 10px;
+  position: absolute;
+  z-index: 1;
+  bottom: 125%; /* Position the tooltip above the element */
+  left: 50%;
+  margin-left: -150px;
+  opacity: 0;
+  transition: opacity 0.3s;
+}
+
+.tooltip:hover .tooltiptext {
+  visibility: visible;
+  opacity: 1;
+}
+
+.tooltip img {
+  height: 40px;
+  width: 40px;
+  border-radius: 20px;
+  margin-right: .5em;
+  margin-bottom: .5em;
+  float: left;
+}
+
+.tooltip p {
+  padding: 0;
+  margin: 0;
+}
+
+.tooltip .tooltiptext .commit-message {
+  font-weight: bold;
+}
+
+.tooltip .tooltiptext .commit-author {
+  font-style: italic;
+  color: #bbb;
+}
+
+.tooltip .tooltiptext .commit-date {
+  color: #bbb;
+}
+
+.tooltip .tooltiptext .commit-sha {
+  font-style: italic;
+  color: #5cb6de;
+}