feat: add MarkdownDisplay

ProofWidgets/Component/Basic.lean

@@ -87,6 +87,27 @@ def InteractiveMessage : Component InteractiveMessageProps where
     }
   "
 
+structure MarkdownDisplay.Props where
+  contents : String
+  deriving ToJson, FromJson
+
+/-- Render a given string as Markdown.
+LaTeX is supported with MathJax:
+use `$...$` for inline math,
+and `$$...$$` for displayed math.
+
+Example usage:
+```lean
+<MarkdownDisplay contents={"$a + b = c$"} />
+``` -/
+@[widget_module]
+def MarkdownDisplay : Component MarkdownDisplay.Props where
+  javascript := "
+    import { Markdown } from '@leanprover/infoview'
+    import * as React from 'react'
+    export default (props) => React.createElement(Markdown, props)
+  "
+
 end ProofWidgets
 
 /-- Construct a structured message from a ProofWidgets component.

ProofWidgets/Demos/Jsx.lean

@@ -21,6 +21,14 @@ def htmlLetters : Array ProofWidgets.Html := #[
 def x := <b>You can use {...htmlLetters} in Lean {.text s!"{1 + 3}"}! <hr/> </b>
 #html x
 
+-- Use `MarkdownDisplay` to render Markdown
+open ProofWidgets in
+#html <MarkdownDisplay contents={"
+  ## Hello, Markdown
+  We have **bold text**, _italic text_, `example : True := by trivial`,
+  and $3×19 = \\int\\limits_0^{57}1~dx$.
+"} />
+
 -- HTML trees can also be produced by metaprograms
 open ProofWidgets Lean Elab in
 #html (do