inductive Lean.Widget.TaggedText (α : Type u) : Type u

The minimal structure needed to represent "string with interesting (tagged) substrings". Much like Lean 3 sf, but with indentation already stringified.

• text {α : Type u} : String → TaggedText α
• append {α : Type u} : Array (TaggedText α) → TaggedText α

  Invariants:

  • non-empty
  • no adjacent text elements (they should be collapsed)
  • no directly nested appends (but append #[tag _ (append ..)] is okay)
• tag {α : Type u} : α → TaggedText α → TaggedText α

instance Lean.Widget.instInhabitedTaggedText {a✝ : Type u_1} : Inhabited (TaggedText a✝)

instance Lean.Widget.instBEqTaggedText {α✝ : Type u_1} [BEq α✝] : BEq (TaggedText α✝)

instance Lean.Widget.instReprTaggedText {α✝ : Type u_1} [Repr α✝] : Repr (TaggedText α✝)

instance Lean.Widget.instFromJsonTaggedText {α✝ : Type} [FromJson α✝] : FromJson (TaggedText α✝)

instance Lean.Widget.instToJsonTaggedText {α✝ : Type u_1} [ToJson α✝] : ToJson (TaggedText α✝)

def Lean.Widget.TaggedText.appendText {α : Type u_1} (s₀ : String) : TaggedText α → TaggedText α

def Lean.Widget.TaggedText.appendTag {α : Type u_1} (acc : TaggedText α) (t₀ : α) (a₀ : TaggedText α) : TaggedText α

partial def Lean.Widget.TaggedText.map {α : Type u_1} {β : Type u_2} (f : α → β) : TaggedText α → TaggedText β

partial def Lean.Widget.TaggedText.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) : TaggedText α → m (TaggedText β)

partial def Lean.Widget.TaggedText.rewrite {α : Type u_1} {β : Type u_2} (f : α → TaggedText α → TaggedText β) : TaggedText α → TaggedText β

partial def Lean.Widget.TaggedText.rewriteM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → TaggedText α → m (TaggedText β)) : TaggedText α → m (TaggedText β)

Like mapM but allows rewriting the whole subtree at tag nodes.

instance Lean.Widget.TaggedText.instRpcEncodable {α : Type} [Server.RpcEncodable α] : Server.RpcEncodable (TaggedText α)

instance Lean.Widget.TaggedText.instInhabitedTaggedState : Inhabited Lean.Widget.TaggedText.TaggedState✝

instance Lean.Widget.TaggedText.instMonadPrettyFormatStateMTaggedState : Std.Format.MonadPrettyFormat (StateM Lean.Widget.TaggedText.TaggedState✝)

def Lean.Widget.TaggedText.prettyTagged (f : Format) (indent : Nat := 0) (w : Nat := Std.Format.defWidth) : TaggedText (Nat × Nat)

The output is tagged with (tag, indent) where tag is from the input Format and indent is the indentation level at this point. The latter is used to print sub-trees accurately by passing it again as the indent argument.

def Lean.Widget.TaggedText.stripTags {α : Type u_1} (tt : TaggedText α) : String

Remove tags, leaving just the pretty-printed string.

partial def Lean.Widget.TaggedText.stripTags.go {α : Type u_1} (acc : String) : Array (TaggedText α) → String