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_reducible]

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

Equations

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

partial def Lean.Widget.instBEqTaggedText.beq {α✝ : Type u_1} [BEq α✝] : TaggedText α✝ → TaggedText α✝ → Bool

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Lean.Widget.instReprTaggedText = { reprPrec := Lean.Widget.instReprTaggedText.repr }

partial def Lean.Widget.instReprTaggedText.repr {α✝ : Type u_1} [Repr α✝] : TaggedText α✝ → Nat → Format

partial def Lean.Widget.instFromJsonTaggedText.fromJson {α✝ : Type} [FromJson α✝] : Json → Except String (TaggedText α✝)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

partial def Lean.Widget.instToJsonTaggedText.toJson {α✝ : Type u_1} [ToJson α✝] : TaggedText α✝ → Json

def Lean.Widget.TaggedText.appendText {α : Type u_1} (s₀ : String) : TaggedText α → 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 : TaggedText α) (t₀ : α) (a₀ : TaggedText α) : 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 : α → β) : 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.forM {m : Type → Type u_1} {α : Type u_2} [Monad m] (f : α → TaggedText α → m Unit) : TaggedText α → m Unit

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_reducible]

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

Equations

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

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.

Equations

• Lean.Widget.TaggedText.prettyTagged f indent w = Lean.Widget.TaggedText.TaggedState.out✝ (StateT.run (f.prettyM w indent) { }).snd

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

Remove tags, leaving just the pretty-printed string.

Equations

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