diff --git a/ProofWidgets/Component/InfoGraph.lean b/ProofWidgets/Component/InfoGraph.lean index 61726c1..01b6393 100644 --- a/ProofWidgets/Component/InfoGraph.lean +++ b/ProofWidgets/Component/InfoGraph.lean @@ -4,17 +4,46 @@ import ProofWidgets.Component.HtmlDisplay open Lean namespace ProofWidgets -structure Node where +structure InfoGraph.Node where id : String html : Html deriving Inhabited, Server.RpcEncodable -structure InfoGraphProps where +structure InfoGraph.Props where nodes : Array Node dot : String defaultHtml : Html deriving Inhabited, Server.RpcEncodable +/-- +This component renders an interactive graphviz graph. + +Users must provide three fields: + +- `nodes : Array InfoGraph.Node` +- `dot : String` +- `defaultHtml : Html` + +Here `InfoGraph.Node` is a structure with two fields: + +- `id : String` +- `html : Html` + +The `nodes` specify the nodes of the graph, `dot` is the contents of a dotfile used +to render the graph itself and `defaultHtml` is the default html which will be rendered +in the information section. + +Example usage: +`` + +This will display the graph specified in the string `dot`. +The component expects that the nodes defined in `dot` all have an `id` +which matches the id field in exactly one of the elements of `nodes`. +When clicking on the node with a given `id`, the html in that particular +node will then be displayed. + +Clicking outside of any node will dislpay the default html (which also appears by default). +-/ @[widget_module] -def InfoGraph : Component InfoGraphProps where +def InfoGraph : Component InfoGraph.Props where javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "infoGraph.js" diff --git a/ProofWidgets/Component/MarkdownWithMathjax.lean b/ProofWidgets/Component/MarkdownWithMathjax.lean index 0f36dd1..944ab2a 100644 --- a/ProofWidgets/Component/MarkdownWithMathjax.lean +++ b/ProofWidgets/Component/MarkdownWithMathjax.lean @@ -4,10 +4,27 @@ open Lean namespace ProofWidgets -structure MarkdownWithMathjaxProps where +structure MarkdownWithMathjax.Props where markdown : String deriving Inhabited, Server.RpcEncodable +/-- +This component renders a markdown string with mathjax. + +Example usage: +```lean + +``` + +Use `$` for inline math and +``` +```math +a + b = c +``` +``` + +for displayed math. +-/ @[widget_module] -def MarkdownWithMathjax : Component MarkdownWithMathjaxProps where +def MarkdownWithMathjax : Component MarkdownWithMathjax.Props where javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "markdownWithMathjax.js" diff --git a/ProofWidgets/Demos/ExprGraph.lean b/ProofWidgets/Demos/ExprGraph.lean index bf1dfcb..ce1f8f4 100644 --- a/ProofWidgets/Demos/ExprGraph.lean +++ b/ProofWidgets/Demos/ExprGraph.lean @@ -2,6 +2,10 @@ import ProofWidgets.Component.InfoGraph import ProofWidgets.Component.MarkdownWithMathjax import Lean +/-! +A simple demo of the `InfoGraph` and `MarkdownWithMathjax` components. +-/ + open ProofWidgets Jsx Lean Server structure MyProps where @@ -22,15 +26,15 @@ def elabExprGraphCmd : CommandElab := fun let some bb := env.find? b | continue if bb.getUsedConstantsAsSet.contains a then edges := edges.insert (a, b) - let mut nodesWithInfos : Array Node := #[] + let mut nodesWithInfos : Array InfoGraph.Node := #[] for node in nodes.toArray do let some c := env.find? node | continue let doc? ← findDocString? env node let ee ← Lean.Widget.ppExprTagged c.type let us ← Meta.mkFreshLevelMVarsFor c let e ← Lean.Widget.ppExprTagged (.const node us) - let newNode : Node := { - id := s!"{hash node}" + let newNode : InfoGraph.Node := { + id := s!"{node}" html := match doc? with | some d =>
@@ -47,7 +51,7 @@ def elabExprGraphCmd : CommandElab := fun for (a,b) in nodes.toArray.zip nodesWithInfos do dot := dot ++ s!" \"{b.id}\" [id=\"{b.id}\", label=\"{a}\"];\n" for (a,b) in edges do - dot := dot ++ s!" \"{hash a}\" -> \"{hash b}\";\n" + dot := dot ++ s!" \"{a}\" -> \"{b}\";\n" dot := dot ++ "}" let defaultHtml : Html :=