Lean4
@[command_elab stringDiagram, inherit_doc stringDiagram]
def elabStringDiagramCmd : CommandElab := fun
| stx@(`(#string_diagram $t:term)) => do
let html ←
runTermElabM fun _ => do
let e ←
try
mkConstWithFreshMVarLevels (← realizeGlobalConstNoOverloadWithInfo t)
catch _ =>
Term.levelMVarToParam (← instantiateMVars (← Term.elabTerm t none))
match ← StringDiagram.stringMorOrEqM? e with
| some html =>
return html
| none =>
throwError "could not find a morphism or equality: {e}"
liftCoreM <|
Widget.savePanelWidgetInfo (hash HtmlDisplay.javascript)
(return json% {html: $(← Server.RpcEncodable.rpcEncode html)}) stx
| stx => throwError "Unexpected syntax {stx}."