TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Widgets.Core.UI

Widgets UI helpers #

Shared HTML formatting, status badges, DOT label escaping, and source-location handling for ProofWidgets viewers. These helpers run in the infoview's meta code, not the model runtime.

References:

source
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.

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

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

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

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

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

        Render a success badge.

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

          Render a warning badge.

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

            Render an error badge.

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

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

              Instances For
                source
                def NN.Widgets.UI.escapeDotLabel (s : String) :
                String

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

                Instances For