Skip to content

Commit

Permalink
feat: improve Markdown popup rendering (#534)
Browse files Browse the repository at this point in the history
- [x] Render math with MathJax
- [x] Highlight Lean syntax with highlight.js
- [ ] ~~Pass theme through from CSS vars to `hljs-*` vars~~ (this
appears impossible, see microsoft/vscode#32813)
- [x] Export `Markdown` component

<img width="308" alt="Screenshot 2024-10-15 at 9 36 24 PM"
src="https://github.com/user-attachments/assets/463cc0fd-dd09-43cd-b596-999577fcac11">
  • Loading branch information
Vtec234 authored Oct 17, 2024
1 parent 276850a commit cd70bdd
Show file tree
Hide file tree
Showing 10 changed files with 6,156 additions and 3,091 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/on-push.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
23 changes: 14 additions & 9 deletions lean4-infoview/package.json
Original file line number Diff line number Diff line change
@@ -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",
Expand All @@ -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"
},
Expand All @@ -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"
Expand Down
2 changes: 2 additions & 0 deletions lean4-infoview/rollup.config.js
Original file line number Diff line number Diff line change
@@ -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'
Expand Down Expand Up @@ -46,6 +47,7 @@ const plugins = [
preventAssignment: true, // TODO delete when `true` becomes the default
}),
commonjs(),
json(),
]

/**
Expand Down
2 changes: 1 addition & 1 deletion lean4-infoview/src/index.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
210 changes: 210 additions & 0 deletions lean4-infoview/src/infoview/highlightjs.css
Original file line number Diff line number Diff line change
@@ -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;
}
2 changes: 1 addition & 1 deletion lean4-infoview/src/infoview/infos.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -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
},
[],
Expand Down
73 changes: 47 additions & 26 deletions lean4-infoview/src/infoview/interactiveCode.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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>
}
Expand Down Expand Up @@ -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. */
Expand Down
Loading

0 comments on commit cd70bdd

Please sign in to comment.