Widgets UI helpers

TorchLean has multiple ProofWidgets-based viewers (IR graphs, autograd tapes, RL rollouts, etc.). Several widgets share the same compact HTML helpers (monospace, pill, status badges, DOT label escaping).

This file centralizes those helpers so:

• widget modules stay consistent,
• style tweaks happen in one place, and
• we avoid “private def …” duplication across many files.

Design notes:

• This is small and explicit and depends only on ProofWidgets.
• These helpers are meta only (used for infoview UI), not part of the executable runtime.

References:

• ProofWidgets: https://github.com/leanprover-community/ProofWidgets4
• GraphViz DOT label escaping rules: https://graphviz.org/doc/info/lang.html

def NN.Widgets.UI.canonicalCommand (stx : Lean.TSyntax `command) : Lean.TSyntax `command

Mark a macro-generated command as the source location of its widget panel.

def NN.Widgets.UI.monospace (s : String) : ProofWidgets.Html

Render a string as monospace code, using VS Code theme fonts when available.

def NN.Widgets.UI.pill (s : String) : ProofWidgets.Html

Render a small “pill” badge (used for compact key/value metadata).

def NN.Widgets.UI.okBadge (s : String) : ProofWidgets.Html

Render a success badge.

def NN.Widgets.UI.warnBadge (s : String) : ProofWidgets.Html

Render a warning badge.

def NN.Widgets.UI.errBadge (s : String) : ProofWidgets.Html

Render an error badge.

def NN.Widgets.UI.flagBadge (name : String) (isSet : Bool) : ProofWidgets.Html

Render a boolean flag: green when set, muted otherwise.

def NN.Widgets.UI.escapeDotLabel (s : String) : String

Escape a string so it is safe to embed inside a double-quoted DOT node label.