feat: Lean syntax highlighting in Markdown

lean4-infoview/package.json

@@ -10,7 +10,7 @@
     },
     "exports": {
         ".": "./dist/index.development.js",
-        "./loader": "./dist/loader.production.min.js",
+        "./loader": "./dist/loader.development.js",
         "./package.json": "./package.json"
     },
     "typesVersions": {
@@ -39,10 +39,12 @@
         "@types/react": "^18.2.15",
         "@types/react-dom": "^18.2.7",
         "current-release": "npm:@leanprover/infoview@latest",
+        "highlightjs-lean": "^1.2.0",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
         "react-markdown": "^9.0.1",
         "remark-math": "^6.0.0",
+        "rehype-highlight": "^7.0.0",
         "rehype-mathjax": "^6.0.0",
         "rollup": "^4.24.0",
         "rollup-plugin-css-only": "^4.3.0",

lean4-infoview/src/infoview/interactiveCode.tsx

@@ -9,7 +9,10 @@ import {
     TaggedText,
     TaggedText_stripTags,
 } from '@leanprover/infoview-api'
+// @ts-ignore
+import leanHljs from 'highlightjs-lean'
 import ReactMarkdown from 'react-markdown'
+import rehypeHighlight from 'rehype-highlight'
 import rehypeMathjax from 'rehype-mathjax'
 import remarkMath from 'remark-math'
 import { Location } from 'vscode-languageserver-protocol'
@@ -73,7 +76,12 @@ function Markdown({ contents }: { contents: string }): JSX.Element {
         <ReactMarkdown
             children={contents}
             remarkPlugins={[remarkMath]}
-            rehypePlugins={[rehypeMathjax]}
+            rehypePlugins={[
+                rehypeMathjax,
+                // NOTE: Instead of rehype-highlight,
+                // we could use rehype-starrynight with the TextMate grammar in this repo
+                opts => rehypeHighlight({ ...opts, languages: { lean: leanHljs } }),
+            ]}
             components={{
                 code(props) {
                     const { children, className, node, ...rest } = props

lean4-infoview/src/infoview/main.tsx

@@ -25,7 +25,7 @@ import { WithRpcSessions } from './rpcSessions'
 import { ServerVersion } from './serverVersion'
 import { useClientNotificationEffect, useEventResult, useServerNotificationState } from './util'
 
-function Main(props: {}) {
+function Main() {
     const ec = React.useContext(EditorContext)
 
     /* Set up updates to the global infoview state on editor events. */