TermColor.Text: styled text and spans

Text is a sequence of styled segments. The representation is deliberately small and transparent: append preserves order, and rendering is a pure fold over the segments.

structure TermColor.Segment : Type

One piece of text with one style overlay.

• text : String

  Visible text in the segment.

• style : Style

  Style applied to the segment.

• link : Option String

  Optional OSC-8 hyperlink URI.

@[instance_reducible]

instance TermColor.instBEqSegment : BEq Segment

Equations

• TermColor.instBEqSegment = { beq := TermColor.instBEqSegment.beq }

def TermColor.instBEqSegment.beq : Segment → Segment → Bool

Equations

• TermColor.instBEqSegment.beq { text := a, style := a_1, link := a_2 } { text := b, style := b_1, link := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.instBEqSegment.beq x✝¹ x✝ = false

def TermColor.instDecidableEqSegment.decEq (x✝ x✝¹ : Segment) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.instDecidableEqSegment : DecidableEq Segment

Equations

• TermColor.instDecidableEqSegment = TermColor.instDecidableEqSegment.decEq

def TermColor.instReprSegment.repr : Segment → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.instReprSegment : Repr Segment

Equations

• TermColor.instReprSegment = { reprPrec := TermColor.instReprSegment.repr }

structure TermColor.Text : Type

Text with styles attached to segments.

• segments : List Segment

  Ordered styled segments.

@[instance_reducible]

instance TermColor.instBEqText : BEq Text

Equations

• TermColor.instBEqText = { beq := TermColor.instBEqText.beq }

def TermColor.instBEqText.beq : Text → Text → Bool

Equations

• TermColor.instBEqText.beq { segments := a } { segments := b } = (a == b)
• TermColor.instBEqText.beq x✝¹ x✝ = false

def TermColor.instDecidableEqText.decEq (x✝ x✝¹ : Text) : Decidable (x✝ = x✝¹)

Equations

• TermColor.instDecidableEqText.decEq { segments := a } { segments := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.instDecidableEqText : DecidableEq Text

Equations

• TermColor.instDecidableEqText = TermColor.instDecidableEqText.decEq

@[instance_reducible]

instance TermColor.instReprText : Repr Text

Equations

• TermColor.instReprText = { reprPrec := TermColor.instReprText.repr }

def TermColor.instReprText.repr : Text → Nat → Std.Format

Equations

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

def TermColor.Text.empty : Text

An empty text value.

Equations

• TermColor.Text.empty = { }

def TermColor.Text.plain (text : String) : Text

Unstyled text.

Equations

• TermColor.Text.plain text = { segments := [{ text := text }] }

def TermColor.Text.styled (text : String) (style : Style) : Text

Text with one style overlay.

Equations

• TermColor.Text.styled text style = { segments := [{ text := text, style := style }] }

def TermColor.Text.hyperlink (uri : String) (text : Text) : Text

Attach a terminal hyperlink to all segments in a text value.

Equations

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

def TermColor.Text.append (left right : Text) : Text

Append two text values without changing their styles.

Equations

• left.append right = { segments := left.segments ++ right.segments }

@[instance_reducible]

instance TermColor.Text.instEmptyCollection : EmptyCollection Text

Equations

• TermColor.Text.instEmptyCollection = { emptyCollection := TermColor.Text.empty }

@[instance_reducible]

instance TermColor.Text.instAppend : Append Text

Equations

• TermColor.Text.instAppend = { append := TermColor.Text.append }

def TermColor.Text.concat (texts : List Text) : Text

Concatenate text values in order.

Equations

• TermColor.Text.concat texts = { segments := List.flatMap (fun (x : TermColor.Text) => x.segments) texts }

def TermColor.Text.perChar (text : String) (style : Nat → Nat → Style) : Text

Style every character of a string from its index and the total character count.

Equations

• TermColor.Text.perChar text style = { segments := List.mapIdx (fun (i : Nat) (c : Char) => { text := c.toString, style := style i text.toList.length }) text.toList }

def TermColor.Text.rainbow (text : String) : Text

Sweep the hue wheel across the characters of a string.

Equations

• TermColor.Text.rainbow text = TermColor.Text.perChar text fun (i n : Nat) => TermColor.Style.fg (TermColor.Color.hue (i * 330 / max n 1))

def TermColor.Text.plainText (text : Text) : String

Remove all ANSI styling while preserving the visible text.

Equations

• text.plainText = String.join (List.map (fun (segment : TermColor.Segment) => segment.text) text.segments)

def TermColor.Text.renderSegment (target : RenderTarget) (segment : Segment) : String

Render one segment for a terminal target.

Equations

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

@[simp]

theorem TermColor.Text.renderSegment_plain (segment : Segment) : renderSegment RenderTarget.plain segment = segment.text

Plain targets preserve text and suppress both styles and hyperlinks.

def TermColor.Text.render (target : RenderTarget) (text : Text) : String

Render styled text, optionally emitting OSC-8 hyperlinks for linked segments.

Equations

• TermColor.Text.render target text = String.join (List.map (fun (segment : TermColor.Segment) => TermColor.Text.renderSegment target segment) text.segments)