structure ProofWidgets.HtmlDisplayProps : Type

• html : Html

instance ProofWidgets.instRpcEncodableHtmlDisplayProps : Lean.Server.RpcEncodable HtmlDisplayProps

def ProofWidgets.HtmlDisplay : Component HtmlDisplayProps

def ProofWidgets.HtmlDisplayPanel : Component HtmlDisplayProps

class ProofWidgets.HtmlEval (α : Type u) : Type u

Any term t : α with a HtmlEval α instance can be evaluated in a #html t command.

This is analogous to how Lean.MetaEval supports #eval.

• eval : α → Lean.Elab.Command.CommandElabM Html

instance ProofWidgets.instHtmlEvalHtml : HtmlEval Html

instance ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM {m : Type → Type u_1} [MonadLiftT m Lean.Elab.Command.CommandElabM] : HtmlEval (m Html)

instance ProofWidgets.instHtmlEvalCoreMHtml : HtmlEval (Lean.CoreM Html)

instance ProofWidgets.instHtmlEvalMetaMHtml : HtmlEval (Lean.MetaM Html)

instance ProofWidgets.instHtmlEvalTermElabMHtml : HtmlEval (Lean.Elab.TermElabM Html)

unsafe def ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe (stx : Lean.Term) : Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM Html)

@[implemented_by ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe]

opaque ProofWidgets.HtmlCommand.evalCommandMHtml : Lean.Term → Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM Html)

def ProofWidgets.HtmlCommand.htmlCmd : Lean.ParserDescr

Display a value of type Html in the infoview.

The input can be a pure value or a computation in any Lean metaprogramming monad (e.g. CommandElabM Html).

def ProofWidgets.HtmlCommand.elabHtmlCmd : Lean.Elab.Command.CommandElab

def Lean.MessageData.ofHtml (h : ProofWidgets.Html) (alt : String) : CoreM MessageData

Construct a structured message from ProofWidgets HTML.

For the meaning of alt, see MessageData.ofWidget.