feat: improve Markdown popup rendering

.github/workflows/on-push.yml

@@ -35,7 +35,7 @@ jobs:
       - name: Setup Node.js
         uses: actions/setup-node@v2
         with:
-          node-version: '16'
+          node-version: '20'
         if: matrix.os == 'windows-latest'
 
       - name: Build

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.7.5",
+    "version": "0.7.6",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -25,20 +25,26 @@
     "type": "module",
     "license": "Apache-2.0",
     "devDependencies": {
-        "@floating-ui/react": "^0.24.7",
-        "@rollup/plugin-commonjs": "^23.0.7",
+        "@floating-ui/react": "^0.26.25",
+        "@rollup/plugin-commonjs": "^28.0.0",
+        "@rollup/plugin-json": "^6.1.0",
         "@rollup/plugin-node-resolve": "^15.1.0",
-        "@rollup/plugin-replace": "^5.0.2",
-        "@rollup/plugin-terser": "^0.1.0",
-        "@rollup/plugin-typescript": "^9.0.2",
+        "@rollup/plugin-replace": "^6.0.1",
+        "@rollup/plugin-terser": "^0.4.4",
+        "@rollup/plugin-typescript": "^12.1.0",
         "@rollup/plugin-url": "^8.0.1",
-        "@types/marked": "^4.3.1",
         "@types/react": "^18.2.15",
         "@types/react-dom": "^18.2.7",
+        "@types/react-syntax-highlighter": "^15.5.13",
         "current-release": "npm:@leanprover/infoview@latest",
+        "highlightjs-lean": "^1.2.0",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
-        "rollup": "^3.26.2",
+        "react-markdown": "^9.0.1",
+        "react-syntax-highlighter": "^15.5.0",
+        "remark-math": "^6.0.0",
+        "rehype-mathjax": "^6.0.0",
+        "rollup": "^4.24.0",
         "rollup-plugin-css-only": "^4.3.0",
         "typescript": "^5.4.5"
     },
@@ -47,7 +53,6 @@
         "@vscode/codicons": "^0.0.32",
         "@vscode/webview-ui-toolkit": "^1.4.0",
         "es-module-shims": "^1.7.3",
-        "marked": "^4.3.0",
         "react-fast-compare": "^3.2.2",
         "tachyons": "^4.12.0",
         "vscode-languageserver-protocol": "^3.17.3"

lean4-infoview/rollup.config.js

@@ -1,4 +1,5 @@
 import commonjs from '@rollup/plugin-commonjs'
+import json from '@rollup/plugin-json'
 import nodeResolve from '@rollup/plugin-node-resolve'
 import replace from '@rollup/plugin-replace'
 import terser from '@rollup/plugin-terser'
@@ -46,6 +47,7 @@ const plugins = [
         preventAssignment: true, // TODO delete when `true` becomes the default
     }),
     commonjs(),
+    json(),
 ]
 
 /**

lean4-infoview/src/index.tsx

@@ -7,7 +7,7 @@ export * from '@leanprover/infoview-api'
 export { EditorContext, EnvPosContext, VersionContext } from './infoview/contexts'
 export { EditorConnection } from './infoview/editorConnection'
 export { GoalLocation, GoalsLocation, LocationsContext } from './infoview/goalLocation'
-export { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode'
+export { InteractiveCode, InteractiveCodeProps, Markdown } from './infoview/interactiveCode'
 export { renderInfoview } from './infoview/main'
 export { RpcContext, useRpcSession } from './infoview/rpcSessions'
 export { ServerVersion } from './infoview/serverVersion'

lean4-infoview/src/infoview/highlightjs.css

@@ -0,0 +1,210 @@
+/*
+This file contains syntax highlighting themes for highlight.js,
+taken from https://unpkg.com/browse/@highlightjs/cdn-assets@11.10.0/styles/github.css (light)
+and https://unpkg.com/browse/@highlightjs/cdn-assets@11.10.0/styles/github-dark.css (dark)
+
+Unfortunately there is no way to retrieve theme colors from VSCode:
+https://github.com/Microsoft/vscode/issues/32813
+*/
+
+pre code.hljs {
+    display: block;
+}
+
+/*!
+  Theme: GitHub
+  Description: Light theme as seen on github.com
+  Author: github.com
+  Maintainer: @Hirse
+  Updated: 2021-05-15
+
+  Outdated base version: https://github.com/primer/github-syntax-light
+  Current colors taken from GitHub's CSS
+*/
+
+.hljs-doctag,
+.hljs-keyword,
+.hljs-meta .hljs-keyword,
+.hljs-template-tag,
+.hljs-template-variable,
+.hljs-type,
+.hljs-variable.language_ {
+    /* prettylights-syntax-keyword */
+    color: #d73a49;
+}
+.hljs-title,
+.hljs-title.class_,
+.hljs-title.class_.inherited__,
+.hljs-title.function_ {
+    /* prettylights-syntax-entity */
+    color: #6f42c1;
+}
+.hljs-attr,
+.hljs-attribute,
+.hljs-literal,
+.hljs-meta,
+.hljs-number,
+.hljs-operator,
+.hljs-variable,
+.hljs-selector-attr,
+.hljs-selector-class,
+.hljs-selector-id {
+    /* prettylights-syntax-constant */
+    color: #005cc5;
+}
+.hljs-regexp,
+.hljs-string,
+.hljs-meta .hljs-string {
+    /* prettylights-syntax-string */
+    color: #032f62;
+}
+.hljs-built_in,
+.hljs-symbol {
+    /* prettylights-syntax-variable */
+    color: #e36209;
+}
+.hljs-comment,
+.hljs-code,
+.hljs-formula {
+    /* prettylights-syntax-comment */
+    color: #6a737d;
+}
+.hljs-name,
+.hljs-quote,
+.hljs-selector-tag,
+.hljs-selector-pseudo {
+    /* prettylights-syntax-entity-tag */
+    color: #22863a;
+}
+.hljs-subst {
+    /* prettylights-syntax-storage-modifier-import */
+    color: #24292e;
+}
+.hljs-section {
+    /* prettylights-syntax-markup-heading */
+    color: #005cc5;
+    font-weight: bold;
+}
+.hljs-bullet {
+    /* prettylights-syntax-markup-list */
+    color: #735c0f;
+}
+.hljs-emphasis {
+    /* prettylights-syntax-markup-italic */
+    color: #24292e;
+    font-style: italic;
+}
+.hljs-strong {
+    /* prettylights-syntax-markup-bold */
+    color: #24292e;
+    font-weight: bold;
+}
+.hljs-addition {
+    /* prettylights-syntax-markup-inserted */
+    color: #22863a;
+    background-color: #f0fff4;
+}
+.hljs-deletion {
+    /* prettylights-syntax-markup-deleted */
+    color: #b31d28;
+    background-color: #ffeef0;
+}
+
+/*!
+  Theme: GitHub Dark
+  Description: Dark theme as seen on github.com
+  Author: github.com
+  Maintainer: @Hirse
+  Updated: 2021-05-15
+
+  Outdated base version: https://github.com/primer/github-syntax-dark
+  Current colors taken from GitHub's CSS
+*/
+
+.vscode-dark .hljs-doctag,
+.vscode-dark .hljs-keyword,
+.vscode-dark .hljs-meta .hljs-keyword,
+.vscode-dark .hljs-template-tag,
+.vscode-dark .hljs-template-variable,
+.vscode-dark .hljs-type,
+.vscode-dark .hljs-variable.language_ {
+    /* prettylights-syntax-keyword */
+    color: #ff7b72;
+}
+.vscode-dark .hljs-title,
+.vscode-dark .hljs-title.class_,
+.vscode-dark .hljs-title.class_.inherited__,
+.vscode-dark .hljs-title.function_ {
+    /* prettylights-syntax-entity */
+    color: #d2a8ff;
+}
+.vscode-dark .hljs-attr,
+.vscode-dark .hljs-attribute,
+.vscode-dark .hljs-literal,
+.vscode-dark .hljs-meta,
+.vscode-dark .hljs-number,
+.vscode-dark .hljs-operator,
+.vscode-dark .hljs-variable,
+.vscode-dark .hljs-selector-attr,
+.vscode-dark .hljs-selector-class,
+.vscode-dark .hljs-selector-id {
+    /* prettylights-syntax-constant */
+    color: #79c0ff;
+}
+.vscode-dark .hljs-regexp,
+.vscode-dark .hljs-string,
+.vscode-dark .hljs-meta .hljs-string {
+    /* prettylights-syntax-string */
+    color: #a5d6ff;
+}
+.vscode-dark .hljs-built_in,
+.vscode-dark .hljs-symbol {
+    /* prettylights-syntax-variable */
+    color: #ffa657;
+}
+.vscode-dark .hljs-comment,
+.vscode-dark .hljs-code,
+.vscode-dark .hljs-formula {
+    /* prettylights-syntax-comment */
+    color: #8b949e;
+}
+.vscode-dark .hljs-name,
+.vscode-dark .hljs-quote,
+.vscode-dark .hljs-selector-tag,
+.vscode-dark .hljs-selector-pseudo {
+    /* prettylights-syntax-entity-tag */
+    color: #7ee787;
+}
+.vscode-dark .hljs-subst {
+    /* prettylights-syntax-storage-modifier-import */
+    color: #c9d1d9;
+}
+.vscode-dark .hljs-section {
+    /* prettylights-syntax-markup-heading */
+    color: #1f6feb;
+    font-weight: bold;
+}
+.vscode-dark .hljs-bullet {
+    /* prettylights-syntax-markup-list */
+    color: #f2cc60;
+}
+.vscode-dark .hljs-emphasis {
+    /* prettylights-syntax-markup-italic */
+    color: #c9d1d9;
+    font-style: italic;
+}
+.vscode-dark .hljs-strong {
+    /* prettylights-syntax-markup-bold */
+    color: #c9d1d9;
+    font-weight: bold;
+}
+.vscode-dark .hljs-addition {
+    /* prettylights-syntax-markup-inserted */
+    color: #aff5b4;
+    background-color: #033a16;
+}
+.vscode-dark .hljs-deletion {
+    /* prettylights-syntax-markup-deleted */
+    color: #ffdcd7;
+    background-color: #67060c;
+}

lean4-infoview/src/infoview/infos.tsx

@@ -84,7 +84,7 @@ export function Infos() {
                 return newPin
             })
 
-            if (changed) return newPins.filter(p => p !== null) as Keyed<DocumentPosition>[]
+            if (changed) return newPins.filter(p => p !== null)
             return pinnedPositions
         },
         [],

lean4-infoview/src/infoview/interactiveCode.tsx

@@ -9,7 +9,12 @@ import {
     TaggedText,
     TaggedText_stripTags,
 } from '@leanprover/infoview-api'
-import { marked } from 'marked'
+// @ts-ignore
+import leanHljs from 'highlightjs-lean'
+import ReactMarkdown from 'react-markdown'
+import { Light as SyntaxHighlighter } from 'react-syntax-highlighter'
+import rehypeMathjax from 'rehype-mathjax'
+import remarkMath from 'remark-math'
 import { Location } from 'vscode-languageserver-protocol'
 import { EditorContext } from './contexts'
 import { GoalsLocation, LocationsContext, SelectableLocationSettings, useSelectableLocation } from './goalLocation'
@@ -18,6 +23,8 @@ import { useRpcSession } from './rpcSessions'
 import { useHoverTooltip, useToggleableTooltip } from './tooltips'
 import { LogicalDomContext, mapRpcError, useAsync, useEvent, useLogicalDomObserver, useOnClickOutside } from './util'
 
+SyntaxHighlighter.registerLanguage('lean', leanHljs)
+
 export interface InteractiveTextComponentProps<T> {
     fmt: TaggedText<T>
 }
@@ -59,31 +66,45 @@ interface TypePopupContentsProps {
     info: SubexprInfo
 }
 
-function Markdown({ contents }: { contents: string }): JSX.Element {
-    const renderer = new marked.Renderer()
-    renderer.code = (code, lang) => {
-        // todo: render Lean code blocks using the lean syntax.json
-        return `<div class="font-code pre-wrap">${code}</div>`
-    }
-    renderer.codespan = code => {
-        return `<code class="font-code">${code}</code>`
-    }
-
-    const markedOptions: marked.MarkedOptions = {}
-    markedOptions.sanitizer = (html: string): string => {
-        return ''
-    }
-    markedOptions.sanitize = true
-    markedOptions.silent = true
-    markedOptions.renderer = renderer
-
-    // todo: vscode also has lots of post render sanitization and hooking up of href clicks and so on.
-    // see https://github.com/microsoft/vscode/blob/main/src/vs/base/browser/markdownRenderer.ts
-
-    const renderedMarkdown = marked.parse(contents, markedOptions)
-    return <div dangerouslySetInnerHTML={{ __html: renderedMarkdown }} />
-    // handy for debugging:
-    // return <div>{ renderedMarkdown } </div>
+/**
+ * Parse the `contents` as Markdown and render the result.
+ *
+ * This component applies some infoview-specific styling
+ * and then passes the content through to a Markdown renderer
+ * (currently `remark`).
+ */
+export function Markdown({ contents }: { contents: string }): JSX.Element {
+    return (
+        <ReactMarkdown
+            children={contents}
+            remarkPlugins={[remarkMath]}
+            rehypePlugins={[rehypeMathjax]}
+            components={{
+                code(props) {
+                    const { children, className, node, ...rest } = props
+                    if (!children) return <code {...rest} className={className} />
+                    const lang = /language-(\w+)/.exec(className || '')
+                    // NOTE: Instead of `react-syntax-highlighter`, we could use
+                    // - `rehype-starrynight` with the TextMate grammar in this repo
+                    // - the Lean server's semantic token capability,
+                    //   if we had code to highlight semantic tokens in the infoview
+                    //   (especially in the tactic state)
+                    return (
+                        // @ts-ignore
+                        <SyntaxHighlighter
+                            {...rest}
+                            language={lang ? lang[1] : 'lean'}
+                            children={String(children).replace(/\n$/, '')}
+                            codeTagProps={{ className: (className || '') + ' font-code overflow-x-auto' }}
+                            wrapLongLines={true}
+                            PreTag="span"
+                            useInlineStyles={false}
+                        />
+                    )
+                },
+            }}
+        />
+    )
 }
 
 /** Shows `explicitValue : itsType` and a docstring if there is one. */