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 → Lean.Widget.TaggedText α
• append: {α : Type u} → Array (Lean.Widget.TaggedText α) → Lean.Widget.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} → α → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α

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

Equations

• Lean.Widget.instInhabitedTaggedText = { default := Lean.Widget.TaggedText.text default }

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

Equations

• Lean.Widget.instBEqTaggedText = { beq := Lean.Widget.beqTaggedText✝ }

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

Equations

• Lean.Widget.instReprTaggedText = { reprPrec := Lean.Widget.reprTaggedText✝ }

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

Equations

• Lean.Widget.instFromJsonTaggedText = { fromJson? := Lean.Widget.fromJsonTaggedText✝ }

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

Equations

• Lean.Widget.instToJsonTaggedText = { toJson := Lean.Widget.toJsonTaggedText✝ }

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Widget.TaggedText.appendText s₀ (Lean.Widget.TaggedText.text s) = Lean.Widget.TaggedText.text (s ++ s₀)
• Lean.Widget.TaggedText.appendText s₀ x = Lean.Widget.TaggedText.append #[x, Lean.Widget.TaggedText.text s₀]

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

Equations

• (Lean.Widget.TaggedText.append as).appendTag t₀ a₀ = Lean.Widget.TaggedText.append (as.push (Lean.Widget.TaggedText.tag t₀ a₀))
• (Lean.Widget.TaggedText.text "").appendTag t₀ a₀ = Lean.Widget.TaggedText.tag t₀ a₀
• acc.appendTag t₀ a₀ = Lean.Widget.TaggedText.append #[acc, Lean.Widget.TaggedText.tag t₀ a₀]

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

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

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

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

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

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

Equations

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

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

Equations

• Lean.Widget.TaggedText.instInhabitedTaggedState = { default := { out := default, tagStack := default, column := default } }

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

Equations

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

def Lean.Widget.TaggedText.prettyTagged (f : Lean.Format) (indent : Nat := 0) (w : Nat := Std.Format.defWidth) : Lean.Widget.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.

Equations

• Lean.Widget.TaggedText.prettyTagged f indent w = (f.prettyM w indent { out := Lean.Widget.TaggedText.text "", tagStack := [], column := 0 }).snd.out

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

Remove tags, leaving just the pretty-printed string.

Equations

• tt.stripTags = Lean.Widget.TaggedText.stripTags.go "" #[tt]

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