diff --git a/Projects/mathlib-demo/lake-manifest.json b/Projects/mathlib-demo/lake-manifest.json index 67629002..e0b6cbbf 100644 --- a/Projects/mathlib-demo/lake-manifest.json +++ b/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", diff --git a/client/src/Popups/Tools.tsx b/client/src/Popups/Tools.tsx index bf558024..53c123bc 100644 --- a/client/src/Popups/Tools.tsx +++ b/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(null) + const [commit, setCommit] = useState() + const [error, setError] = useState() + + 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 {pkg.rev.substring(0,7)} +
+ { error ? +

{error}

: + (loaded && commit) ? <> + {/* valid */} + +

+ {new Date(commit?.commit?.author?.date).toLocaleString()}
+ {commit?.commit?.message.split('\n')[0]} by {commit?.commit?.author?.name}
+ {commit?.sha} +

+ :

Loading…

+ } +
+
+} + +/** 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<{ {pkg.name} { pkg.type == 'git' ? <> - {pkg.rev.substring(0,7)} + {pkg.inputRev} : (local package) } diff --git a/client/src/css/Editor.css b/client/src/css/Editor.css index f87ed78e..492abcd2 100644 --- a/client/src/css/Editor.css +++ b/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); } diff --git a/client/src/css/Navigation.css b/client/src/css/Navigation.css index f2cf0e03..139604e6 100644 --- a/client/src/css/Navigation.css +++ b/client/src/css/Navigation.css @@ -90,4 +90,63 @@ nav .nav-link:hover { nav select { margin-left: .5rem; margin-right: .5rem; -} \ No newline at end of file +} + +.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; +}