- expr: Lean.Widget.CodeWithInfos → Lean.Widget.MsgEmbed
A piece of Lean code with elaboration/typing data. Note: does not necessarily correspond to an
Expr, the name is for RPC API compatibility.
- goal: Lean.Widget.InteractiveGoal → Lean.Widget.MsgEmbed
An interactive goal display.
- trace: Nat →
Lean.Widget.TaggedText Lean.Widget.MsgEmbed →
Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
(Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow the user to expand sub-traces interactively.
message field is the text of a message possibly containing interactive embeds of type
MsgEmbed. We maintain the invariant that embeds are stored in
.tags with empty
.tag embed (.text ""), because a
MsgEmbed display involve more than just text.
msgToInteractiveAux we produce a
Format object whose
.tag nodes refer to
objects stored in an auxiliary array. Only the most shallow
.tag in every branch through the
Format corresponds to an
EmbedFmt. The kind of this tag determines how the nested
object (possibly including further
.tags), is processed. For example, if the output is
.tag (.expr ctx infos) fmt then tags in the nested
fmt object refer to elements of
In the second stage, we recursively transform such a
TaggedText MsgEmbed according
to the rule above by first pretty-printing it and then grabbing data referenced by the tags from
all the nested arrays (such as the
infos array in the example above).
We cannot easily do the translation in a single
MessageData → TaggedText MsgEmbed step because
that would effectively require reimplementing the (stateful, to keep track of indentation)