Add docstrings

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:
+`<InfoGraph nodes={nodes} dot={dot} defaultHtml={defaultHtml} />`
+
+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"

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
+<MarkdownWithMathjax markdown={"$a + b = c$"} />
+```
+
+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"

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 =>
               <div>
@@ -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 :=
       <MarkdownWithMathjax markdown={"# Click on one of the nodes!"}/>