Adding functionality to render Latex as SVG.

ProofWidgets.lean

@@ -3,6 +3,7 @@ import ProofWidgets.Component.Basic
 import ProofWidgets.Component.FilterDetails
 import ProofWidgets.Component.HtmlDisplay
 import ProofWidgets.Component.InteractiveSvg
+import ProofWidgets.Component.Latex
 import ProofWidgets.Component.MakeEditLink
 import ProofWidgets.Component.OfRpcMethod
 import ProofWidgets.Component.Panel.Basic

ProofWidgets/Component/Latex.lean

@@ -0,0 +1,17 @@
+import Lean.Server.Rpc.Basic
+
+import ProofWidgets.Component.Basic
+
+namespace ProofWidgets
+
+open Lean Server
+
+structure LatexProps where
+  content : String
+  deriving Server.RpcEncodable
+
+@[widget_module]
+def Latex : Component LatexProps where
+  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "latexToSvg.js"
+
+end ProofWidgets

ProofWidgets/Demos/LatexExpr.lean

@@ -0,0 +1,29 @@
+import ProofWidgets.Component.Panel.GoalTypePanel
+import ProofWidgets.Component.Panel.SelectionPanel  -- Needed for GoalTypePanel
+import ProofWidgets.Component.HtmlDisplay
+import ProofWidgets.Component.Latex
+import ProofWidgets.Demos.Macro
+
+open ProofWidgets Jsx Lean
+
+@[expr_presenter]
+def latex_presenter : ExprPresenter where
+  userName := "Latex"
+  layoutKind := .inline
+  present e :=
+    return <span>
+        <Latex content={(← Lean.Meta.ppExpr e).pretty} />
+      </span>
+
+example : 2 + 2 = 4 ∧ 3 + 3 = 6 := by
+  with_panel_widgets [GoalTypePanel]
+    -- Place cursor here.
+    constructor
+    rfl
+    rfl
+
+macro "#latex " src:term : command =>
+  Lean.TSyntax.mkInfoCanonical <$>
+    `(#html <Latex content={$src} />)
+
+#latex "\\mbox{This is a latex string: }\\forall x \\in \\mathbb{N}, x\\ge 0,\\, \\mbox{ rendered as SVG.}"

widget/src/exprPresentation.tsx

@@ -4,6 +4,36 @@ import { RpcContext, RpcSessionAtPos, RpcPtr, Name, DocumentPosition, mapRpcErro
 import HtmlDisplay, { Html } from './htmlDisplay'
 import InteractiveExpr from './interactiveExpr'
 
+import { mathjax } from 'mathjax-full/js/mathjax'
+import { TeX } from 'mathjax-full/js/input/tex'
+import { SVG } from 'mathjax-full/js/output/svg'
+import { AllPackages } from 'mathjax-full/js/input/tex/AllPackages'
+import { liteAdaptor } from 'mathjax-full/js/adaptors/liteAdaptor'
+import { RegisterHTMLHandler } from 'mathjax-full/js/handlers/html'
+
+const adaptor = liteAdaptor()
+RegisterHTMLHandler(adaptor)
+
+const mathjax_document = mathjax.document('', {
+  InputJax: new TeX({ packages: AllPackages }),
+  OutputJax: new SVG({ fontCache: 'local' })
+})
+
+const mathjax_options = {
+  em: 16,
+  ex: 8,
+  containerWidth: 1280
+}
+
+function get_mathjax_svg(math: string): string {
+  const node = mathjax_document.convert(math, mathjax_options)
+  return adaptor.outerHTML(node)
+}
+
+export function RenderLatexSvg({content}: {content: string}): JSX.Element {
+  return <div dangerouslySetInnerHTML={{ __html: get_mathjax_svg(content) }} />
+}
+
 type ExprWithCtx = RpcPtr<'ProofWidgets.ExprWithCtx'>
 
 interface ExprPresentationData {

widget/src/latexToSvg.tsx

@@ -0,0 +1,5 @@
+import { RenderLatexSvg } from "./exprPresentation";
+
+export default function ({content}: {content: string}) {
+  return <RenderLatexSvg content={content} />
+}