Lean.Widget.TaggedText

inductive Lean.Widget.TaggedText (α : 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 α

Instances For

source

def Lean.Widget.instInhabitedTaggedText.default {a✝ : Type u_1} :

TaggedText a✝

Instances For

source

@[implicit_reducible]

instance Lean.Widget.instInhabitedTaggedText {a✝ : Type u_1} :

Inhabited (TaggedText a✝)

source

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

TaggedText α✝ → TaggedText α✝ → Bool

source

@[implicit_reducible]

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

BEq (TaggedText α✝)

source

@[implicit_reducible]

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

Repr (TaggedText α✝)

source

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

TaggedText α✝ → Nat → Format

source

@[implicit_reducible]

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

FromJson (TaggedText α✝)

source

partial def Lean.Widget.instFromJsonTaggedText.fromJson {α✝ : Type} [FromJson α✝] :

Json → Except String (TaggedText α✝)

source

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

TaggedText α✝ → Json

source

@[implicit_reducible]

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

ToJson (TaggedText α✝)

source

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

TaggedText α → TaggedText α

Instances For

source

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

TaggedText α

Instances For

source

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

TaggedText α → TaggedText β

source

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 β)

source

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

TaggedText α → m Unit

source

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

TaggedText α → TaggedText β

source

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.

source

@[implicit_reducible]

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

Server.RpcEncodable (TaggedText α)

source

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.

Instances For

source

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

String

Remove tags, leaving just the pretty-printed string.

Instances For