Documentation

Lean.Widget.InteractiveDiagnostic

inductive Lean.Widget.StrictOrLazy (α : Type) (β : Type) :
Instances For
    instance Lean.Widget.instInhabitedStrictOrLazy :
    {a : Type} → [inst : Inhabited a] → {a_1 : Type} → Inhabited (Lean.Widget.StrictOrLazy a a_1)
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      @[inline, reducible]

      The 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 .text subtrees, i.e. .tag embed (.text ""), because a MsgEmbed display involve more than just text.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The msgToInteractive algorithm turns a MessageData into TaggedText MsgEmbed in two stages.

            First, in msgToInteractiveAux we produce a Format object whose .tag nodes refer to EmbedFmt 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 Format 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 infos.

            In the second stage, we recursively transform such a Format into 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) Format.prettyM algorithm.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Transform a Lean Message concerning the given text into an LSP Diagnostic.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For