- text: {α : Type u} → String → Lean.Widget.TaggedText α
- append: {α : Type u} → Array (Lean.Widget.TaggedText α) → Lean.Widget.TaggedText α
- tag: {α : Type u} → α → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α
instance
Lean.Widget.instToJsonTaggedText
:
{α : Type u_1} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instToJsonTaggedText = { toJson := [anonymous] }
instance
Lean.Widget.instReprTaggedText
:
{α : Type u_1} → [inst : Repr α] → Repr (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instReprTaggedText = { reprPrec := [anonymous] }
instance
Lean.Widget.instFromJsonTaggedText
:
{α : Type} → [inst : Lean.FromJson α] → Lean.FromJson (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instFromJsonTaggedText = { fromJson? := [anonymous] }
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} → [inst : BEq α] → BEq (Lean.Widget.TaggedText α)
Equations
- Lean.Widget.instBEqTaggedText = { beq := [anonymous] }
Equations
- Lean.Widget.TaggedText.appendText s₀ x = match x with | Lean.Widget.TaggedText.text s => Lean.Widget.TaggedText.text (s ++ s₀) | Lean.Widget.TaggedText.append as => match Array.back as with | Lean.Widget.TaggedText.text s => Lean.Widget.TaggedText.append (Array.set! as (Array.size as - 1) (Lean.Widget.TaggedText.text (s ++ s₀))) | a => Lean.Widget.TaggedText.append (Array.push as (Lean.Widget.TaggedText.text s₀)) | a => Lean.Widget.TaggedText.append #[a, Lean.Widget.TaggedText.text s₀]
def
Lean.Widget.TaggedText.appendTag
{α : Type u_1}
(acc : Lean.Widget.TaggedText α)
(t₀ : α)
(a₀ : Lean.Widget.TaggedText α)
:
Equations
- Lean.Widget.TaggedText.appendTag acc t₀ a₀ = match acc with | Lean.Widget.TaggedText.append as => Lean.Widget.TaggedText.append (Array.push as (Lean.Widget.TaggedText.tag t₀ a₀)) | Lean.Widget.TaggedText.text "" => Lean.Widget.TaggedText.tag t₀ a₀ | a => Lean.Widget.TaggedText.append #[a, Lean.Widget.TaggedText.tag t₀ a₀]
partial def
Lean.Widget.TaggedText.mapM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[inst : 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 β)
:
partial def
Lean.Widget.TaggedText.rewriteM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[inst : Monad m]
(f : α → Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β))
:
Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β)
instance
Lean.Widget.TaggedText.instRpcEncodingTaggedText
{α : Type}
{β : outParam Type}
[inst : Lean.Server.RpcEncoding α β]
:
Equations
- Lean.Widget.TaggedText.instRpcEncodingTaggedText = { rpcEncode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => Lean.Widget.TaggedText.mapM Lean.Server.rpcEncode a, rpcDecode := fun {m} [Monad m] [Lean.Server.MonadRpcSession m] a => Lean.Widget.TaggedText.mapM Lean.Server.rpcDecode a }
Equations
- Lean.Widget.TaggedText.instInhabitedTaggedState = { default := { out := default, tagStack := default, column := default } }
Equations
- Lean.Widget.TaggedText.instMonadPrettyFormatStateMTaggedState = { pushOutput := fun s => modify fun x => match x with | { out := out, tagStack := ts, column := col } => { out := Lean.Widget.TaggedText.appendText s out, tagStack := ts, column := col + String.length s }, pushNewline := fun indent => modify fun x => match x with | { out := out, tagStack := ts, column := col } => { out := Lean.Widget.TaggedText.appendText (String.pushn "\n" (Char.ofNat 32) indent) out, tagStack := ts, column := indent }, currColumn := do let a ← get pure a.column, startTag := fun n => modify fun x => match x with | { out := out, tagStack := ts, column := col } => { out := Lean.Widget.TaggedText.text "", tagStack := (n, col, out) :: ts, column := col }, endTags := fun n => modify fun x => match x with | { out := out, tagStack := ts, column := col } => let x := (List.take n ts, List.drop n ts); match x with | (ended, left) => let out' := List.foldl (fun acc x => match x with | (n, col', top) => Lean.Widget.TaggedText.appendTag top (n, col') acc) out ended; { out := out', tagStack := left, column := col } }
def
Lean.Widget.TaggedText.prettyTagged
(f : Lean.Format)
(indent : optParam Nat 0)
(w : optParam Nat Std.Format.defWidth)
:
Equations
- Lean.Widget.TaggedText.prettyTagged f indent w = (Std.Format.prettyM f w indent { out := Lean.Widget.TaggedText.text "", tagStack := [], column := 0 }).snd.out
Equations
- Lean.Widget.TaggedText.stripTags tt = (fun go => go "" #[tt]) Lean.Widget.TaggedText.stripTags.go