cleanup demo

ProofWidgets/Demos/ExprGraph.lean

@@ -27,17 +27,19 @@ def elabExprGraphCmd : CommandElab := fun
       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}"
         html := match doc? with
             | some d =>
               <div>
-                <InteractiveCode fmt = {ee} />
+                <InteractiveCode fmt = {e} />{.text " : "}<InteractiveCode fmt = {ee} />
                 <MarkdownWithMathjax markdown = {d} />
               </div>
             | none =>
               <div>
-                <InteractiveCode fmt = {ee} />
+                <InteractiveCode fmt = {e} />{.text " : "}<InteractiveCode fmt = {ee} />
               </div>
       }
       nodesWithInfos := nodesWithInfos.push newNode
@@ -47,8 +49,13 @@ def elabExprGraphCmd : CommandElab := fun
     for (a,b) in edges do
       dot := dot ++ s!"  \"{hash a}\" -> \"{hash b}\";\n"
     dot := dot ++ "}"
-    let defaultHtml : Html := <p>Default</p>
-    let html : Html := <InfoGraph nodes = {nodesWithInfos} dot = {dot} defaultHtml = {defaultHtml} />
+    let defaultHtml : Html :=
+      <MarkdownWithMathjax markdown={"# Click on one of the nodes!"}/>
+    let html : Html := <InfoGraph
+      nodes = {nodesWithInfos}
+      dot = {dot}
+      defaultHtml = {defaultHtml}
+    />
     Widget.savePanelWidgetInfo
       (hash HtmlDisplayPanel.javascript)
       (return json% { html : $(← Server.rpcEncode html) })
@@ -59,6 +66,6 @@ def a : Nat := 0
 
 def b : Nat := 1
 
-def foo (c : Nat) : Nat := a + b * c
+def foo (c : Nat) : Nat × Int := (a + b * c, a / b)
 
 #expr_graph foo