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 intentionally lightweight 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.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 an “OK” badge with accent color.

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" badge: green when true, muted when false.

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

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