From b67fdf69b93353d57b676ecef7bdeb742416cd04 Mon Sep 17 00:00:00 2001
From: obousquet <obousquet@gmail.com>
Date: Fri, 17 May 2024 20:35:13 +0000
Subject: [PATCH 1/5] Adding functionality to render latex as SVG.

---
 widget/src/exprPresentation.tsx | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/widget/src/exprPresentation.tsx b/widget/src/exprPresentation.tsx
index 20336cd..0ede763 100644
--- a/widget/src/exprPresentation.tsx
+++ b/widget/src/exprPresentation.tsx
@@ -4,6 +4,38 @@ 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 { CHTML } from 'mathjax-full/js/output/chtml'
+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 RenderLatex({content}: {content: string}): JSX.Element {
+  // For explanation of flow-root see https://stackoverflow.com/a/32301823
+  return <div dangerouslySetInnerHTML={{ __html: get_mathjax_svg(content) }} />}</div>
+}
+
 type ExprWithCtx = RpcPtr<'ProofWidgets.ExprWithCtx'>
 
 interface ExprPresentationData {

From 4785ad845a53ece625682d07711ce0ce4514ff93 Mon Sep 17 00:00:00 2001
From: obousquet <obousquet@gmail.com>
Date: Fri, 17 May 2024 21:18:48 +0000
Subject: [PATCH 2/5] Test adding a component for latex.

---
 ProofWidgets/Demos/ExprPresentation.lean | 18 ++++++++++++++++++
 widget/src/latexToSvg.tsx                |  5 +++++
 2 files changed, 23 insertions(+)
 create mode 100644 widget/src/latexToSvg.tsx

diff --git a/ProofWidgets/Demos/ExprPresentation.lean b/ProofWidgets/Demos/ExprPresentation.lean
index 47ee34d..1a1dc74 100644
--- a/ProofWidgets/Demos/ExprPresentation.lean
+++ b/ProofWidgets/Demos/ExprPresentation.lean
@@ -3,6 +3,24 @@ import ProofWidgets.Component.Panel.GoalTypePanel
 
 open ProofWidgets Jsx
 
+structure LatexProps where
+  content : string
+  deriving Server.RpcEncodable
+
+@[widget_module]
+def Latex : Component LatexProps where
+  javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "latexToSvg.js"
+
+@[expr_presenter]
+def latex_presenter : ExprPresenter where
+  userName := "Latex"
+  layoutKind := .inline
+  present e :=
+    return <span>
+        {.text "🐙 "}<Latex content={← Lean.Widget.ppExprTagged e} />{.text " 🐙"}
+      </span>
+
+
 @[expr_presenter]
 def presenter : ExprPresenter where
   userName := "With octopodes"
diff --git a/widget/src/latexToSvg.tsx b/widget/src/latexToSvg.tsx
new file mode 100644
index 0000000..c69dba1
--- /dev/null
+++ b/widget/src/latexToSvg.tsx
@@ -0,0 +1,5 @@
+import { RenderLatex } from "./exprPresentation";
+
+export default function ({content}: {content: string}) {
+  return <RenderLatex content=""/>
+}

From e1b334096e9b8ff0dd09c28658672a9ee678dc0a Mon Sep 17 00:00:00 2001
From: obousquet <obousquet@gmail.com>
Date: Fri, 17 May 2024 21:54:49 +0000
Subject: [PATCH 3/5] Test with raw latex.

---
 ProofWidgets/Demos/ExprPresentation.lean | 16 ++++++++++++----
 widget/src/exprPresentation.tsx          |  2 +-
 widget/src/latexToSvg.tsx                |  2 +-
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/ProofWidgets/Demos/ExprPresentation.lean b/ProofWidgets/Demos/ExprPresentation.lean
index 1a1dc74..e331077 100644
--- a/ProofWidgets/Demos/ExprPresentation.lean
+++ b/ProofWidgets/Demos/ExprPresentation.lean
@@ -1,15 +1,15 @@
 import ProofWidgets.Component.Panel.SelectionPanel
 import ProofWidgets.Component.Panel.GoalTypePanel
 
-open ProofWidgets Jsx
+open ProofWidgets Jsx Lean Server
 
 structure LatexProps where
-  content : string
+  content : String
   deriving Server.RpcEncodable
 
 @[widget_module]
 def Latex : Component LatexProps where
-  javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "latexToSvg.js"
+  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "latexToSvg.js"
 
 @[expr_presenter]
 def latex_presenter : ExprPresenter where
@@ -17,9 +17,17 @@ def latex_presenter : ExprPresenter where
   layoutKind := .inline
   present e :=
     return <span>
-        {.text "🐙 "}<Latex content={← Lean.Widget.ppExprTagged e} />{.text " 🐙"}
+        {.text "🐙 "}<Latex content={(← Lean.Meta.ppExpr e).pretty} />{.text " 🐙"}
       </span>
 
+@[expr_presenter]
+def latex_presenter2 : ExprPresenter where
+  userName := "Latex2"
+  layoutKind := .block
+  present e :=
+    return <span>
+        {.text "🐙 "}<Latex content="\\frac{1}{2}\\mbox{hello, we will prove that } \\begin{align}a sdfs&=&sdfsb\\\\c&d&i\\end{align}" />{.text " 🐙"}
+      </span>
 
 @[expr_presenter]
 def presenter : ExprPresenter where
diff --git a/widget/src/exprPresentation.tsx b/widget/src/exprPresentation.tsx
index 0ede763..f80d6d0 100644
--- a/widget/src/exprPresentation.tsx
+++ b/widget/src/exprPresentation.tsx
@@ -33,7 +33,7 @@ function get_mathjax_svg(math: string): string {
 
 export function RenderLatex({content}: {content: string}): JSX.Element {
   // For explanation of flow-root see https://stackoverflow.com/a/32301823
-  return <div dangerouslySetInnerHTML={{ __html: get_mathjax_svg(content) }} />}</div>
+  return <div dangerouslySetInnerHTML={{ __html: get_mathjax_svg(content) }} />
 }
 
 type ExprWithCtx = RpcPtr<'ProofWidgets.ExprWithCtx'>
diff --git a/widget/src/latexToSvg.tsx b/widget/src/latexToSvg.tsx
index c69dba1..8d24320 100644
--- a/widget/src/latexToSvg.tsx
+++ b/widget/src/latexToSvg.tsx
@@ -1,5 +1,5 @@
 import { RenderLatex } from "./exprPresentation";
 
 export default function ({content}: {content: string}) {
-  return <RenderLatex content=""/>
+  return <RenderLatex content={content} />
 }

From cad5f66b5888351b96552fe57d77323bed151732 Mon Sep 17 00:00:00 2001
From: obousquet <obousquet@gmail.com>
Date: Sat, 18 May 2024 14:57:58 +0000
Subject: [PATCH 4/5] Reorganizing the files for latex rendering.

---
 ProofWidgets.lean                        |  1 +
 ProofWidgets/Component/Latex.lean        | 17 ++++++++++++++
 ProofWidgets/Demos/ExprPresentation.lean | 28 +-----------------------
 ProofWidgets/Demos/LatexExpr.lean        | 28 ++++++++++++++++++++++++
 widget/src/exprPresentation.tsx          |  4 +---
 widget/src/latexToSvg.tsx                |  4 ++--
 6 files changed, 50 insertions(+), 32 deletions(-)
 create mode 100644 ProofWidgets/Component/Latex.lean
 create mode 100644 ProofWidgets/Demos/LatexExpr.lean

diff --git a/ProofWidgets.lean b/ProofWidgets.lean
index de33c78..6de670b 100644
--- a/ProofWidgets.lean
+++ b/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
diff --git a/ProofWidgets/Component/Latex.lean b/ProofWidgets/Component/Latex.lean
new file mode 100644
index 0000000..3dc6346
--- /dev/null
+++ b/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
diff --git a/ProofWidgets/Demos/ExprPresentation.lean b/ProofWidgets/Demos/ExprPresentation.lean
index e331077..47ee34d 100644
--- a/ProofWidgets/Demos/ExprPresentation.lean
+++ b/ProofWidgets/Demos/ExprPresentation.lean
@@ -1,33 +1,7 @@
 import ProofWidgets.Component.Panel.SelectionPanel
 import ProofWidgets.Component.Panel.GoalTypePanel
 
-open ProofWidgets Jsx 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"
-
-@[expr_presenter]
-def latex_presenter : ExprPresenter where
-  userName := "Latex"
-  layoutKind := .inline
-  present e :=
-    return <span>
-        {.text "🐙 "}<Latex content={(← Lean.Meta.ppExpr e).pretty} />{.text " 🐙"}
-      </span>
-
-@[expr_presenter]
-def latex_presenter2 : ExprPresenter where
-  userName := "Latex2"
-  layoutKind := .block
-  present e :=
-    return <span>
-        {.text "🐙 "}<Latex content="\\frac{1}{2}\\mbox{hello, we will prove that } \\begin{align}a sdfs&=&sdfsb\\\\c&d&i\\end{align}" />{.text " 🐙"}
-      </span>
+open ProofWidgets Jsx
 
 @[expr_presenter]
 def presenter : ExprPresenter where
diff --git a/ProofWidgets/Demos/LatexExpr.lean b/ProofWidgets/Demos/LatexExpr.lean
new file mode 100644
index 0000000..4333db9
--- /dev/null
+++ b/ProofWidgets/Demos/LatexExpr.lean
@@ -0,0 +1,28 @@
+import ProofWidgets.Component.Panel.GoalTypePanel
+import ProofWidgets.Component.HtmlDisplay
+import ProofWidgets.Component.Latex
+import ProofWidgets.Presentation.Expr
+
+open ProofWidgets Jsx
+
+@[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 " text: String : command =>
+  Lean.TSyntax.mkInfoCanonical <$>
+    `(#html <Latex content={$text} />)
+
+#latex "\\mbox{This is Latex: }\\forall x \\in \\mathbb{N}, x\\ge 0,\, \\mbox{ rendered as SVG.}"
diff --git a/widget/src/exprPresentation.tsx b/widget/src/exprPresentation.tsx
index f80d6d0..6a3d2d8 100644
--- a/widget/src/exprPresentation.tsx
+++ b/widget/src/exprPresentation.tsx
@@ -6,7 +6,6 @@ import InteractiveExpr from './interactiveExpr'
 
 import { mathjax } from 'mathjax-full/js/mathjax'
 import { TeX } from 'mathjax-full/js/input/tex'
-import { CHTML } from 'mathjax-full/js/output/chtml'
 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'
@@ -31,8 +30,7 @@ function get_mathjax_svg(math: string): string {
   return adaptor.outerHTML(node)
 }
 
-export function RenderLatex({content}: {content: string}): JSX.Element {
-  // For explanation of flow-root see https://stackoverflow.com/a/32301823
+export function RenderLatexSvg({content}: {content: string}): JSX.Element {
   return <div dangerouslySetInnerHTML={{ __html: get_mathjax_svg(content) }} />
 }
 
diff --git a/widget/src/latexToSvg.tsx b/widget/src/latexToSvg.tsx
index 8d24320..bd50475 100644
--- a/widget/src/latexToSvg.tsx
+++ b/widget/src/latexToSvg.tsx
@@ -1,5 +1,5 @@
-import { RenderLatex } from "./exprPresentation";
+import { RenderLatexSvg } from "./exprPresentation";
 
 export default function ({content}: {content: string}) {
-  return <RenderLatex content={content} />
+  return <RenderLatexSvg content={content} />
 }

From 3725e33515c093f8a48669bbd16b15a6eabc7e5b Mon Sep 17 00:00:00 2001
From: obousquet <obousquet@gmail.com>
Date: Sat, 18 May 2024 15:14:36 +0000
Subject: [PATCH 5/5] Bug fix.

---
 ProofWidgets/Demos/LatexExpr.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/ProofWidgets/Demos/LatexExpr.lean b/ProofWidgets/Demos/LatexExpr.lean
index 4333db9..b2b2cb6 100644
--- a/ProofWidgets/Demos/LatexExpr.lean
+++ b/ProofWidgets/Demos/LatexExpr.lean
@@ -1,9 +1,10 @@
 import ProofWidgets.Component.Panel.GoalTypePanel
+import ProofWidgets.Component.Panel.SelectionPanel  -- Needed for GoalTypePanel
 import ProofWidgets.Component.HtmlDisplay
 import ProofWidgets.Component.Latex
-import ProofWidgets.Presentation.Expr
+import ProofWidgets.Demos.Macro
 
-open ProofWidgets Jsx
+open ProofWidgets Jsx Lean
 
 @[expr_presenter]
 def latex_presenter : ExprPresenter where
@@ -21,8 +22,8 @@ example : 2 + 2 = 4 ∧ 3 + 3 = 6 := by
     rfl
     rfl
 
-macro "#latex " text: String : command =>
+macro "#latex " src:term : command =>
   Lean.TSyntax.mkInfoCanonical <$>
-    `(#html <Latex content={$text} />)
+    `(#html <Latex content={$src} />)
 
-#latex "\\mbox{This is Latex: }\\forall x \\in \\mathbb{N}, x\\ge 0,\, \\mbox{ rendered as SVG.}"
+#latex "\\mbox{This is a latex string: }\\forall x \\in \\mathbb{N}, x\\ge 0,\\, \\mbox{ rendered as SVG.}"