TermColor.Ansi: pure ANSI SGR encoding

This module has no terminal detection and performs no IO. A RenderTarget makes the fallback policy explicit, so the same styled value can be rendered as plain text, ANSI-16, ANSI-256, or true color, with optional OSC-8 hyperlinks.

structure TermColor.RenderTarget : Type

Whether styles are emitted, and how much color precision is available.

• styles : Bool

  Whether SGR styles are emitted.

• colors : ColorLevel

  Maximum color precision available to the renderer.

• hyperlinks : Bool

  Whether OSC-8 hyperlinks are emitted.

def TermColor.instBEqRenderTarget.beq : RenderTarget → RenderTarget → Bool

Equations

• TermColor.instBEqRenderTarget.beq { styles := a, colors := a_1, hyperlinks := a_2 } { styles := b, colors := b_1, hyperlinks := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• TermColor.instBEqRenderTarget.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.instBEqRenderTarget : BEq RenderTarget

Equations

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

@[instance_reducible]

instance TermColor.instDecidableEqRenderTarget : DecidableEq RenderTarget

Equations

• TermColor.instDecidableEqRenderTarget = TermColor.instDecidableEqRenderTarget.decEq

def TermColor.instDecidableEqRenderTarget.decEq (x✝ x✝¹ : RenderTarget) : Decidable (x✝ = x✝¹)

Equations

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

def TermColor.instReprRenderTarget.repr : RenderTarget → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TermColor.instReprRenderTarget : Repr RenderTarget

Equations

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

def TermColor.RenderTarget.plain : RenderTarget

A plain-text target with no styles or colors.

Equations

• TermColor.RenderTarget.plain = { styles := false, colors := TermColor.ColorLevel.none }

def TermColor.RenderTarget.ansi16 : RenderTarget

An ANSI-16 target.

Equations

• TermColor.RenderTarget.ansi16 = { colors := TermColor.ColorLevel.ansi16 }

def TermColor.RenderTarget.ansi256 : RenderTarget

An xterm 256-color target.

Equations

• TermColor.RenderTarget.ansi256 = { colors := TermColor.ColorLevel.ansi256 }

def TermColor.RenderTarget.trueColor : RenderTarget

A true-color target.

Equations

• TermColor.RenderTarget.trueColor = { }

def TermColor.RenderTarget.withHyperlinks (target : RenderTarget) : RenderTarget

Enable OSC-8 hyperlinks while preserving the target's color and style policy.

Equations

• target.withHyperlinks = { styles := target.styles, colors := target.colors, hyperlinks := true }

inductive TermColor.Layer : Type

The SGR layer to which a color is applied.

• foreground : Layer

  The foreground SGR layer.

• background : Layer

  The background SGR layer.

@[instance_reducible]

instance TermColor.instBEqLayer : BEq Layer

Equations

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

def TermColor.instBEqLayer.beq : Layer → Layer → Bool

Equations

• TermColor.instBEqLayer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance TermColor.instDecidableEqLayer : DecidableEq Layer

Equations

• TermColor.instDecidableEqLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TermColor.instReprLayer.repr : Layer → Nat → Std.Format

Equations

• TermColor.instReprLayer.repr TermColor.Layer.foreground prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Layer.foreground")).group prec✝
• TermColor.instReprLayer.repr TermColor.Layer.background prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Layer.background")).group prec✝

@[instance_reducible]

instance TermColor.instReprLayer : Repr Layer

Equations

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

def TermColor.Color.sgrCodes (layer : Layer) (level : ColorLevel) (color : Color) : List Nat

Encode a color for one SGR layer at a given terminal color level.

Equations

• TermColor.Color.sgrCodes layer TermColor.ColorLevel.none color = []
• TermColor.Color.sgrCodes layer TermColor.ColorLevel.ansi16 color = TermColor.Color.ansi16Codes✝ layer color
• TermColor.Color.sgrCodes layer TermColor.ColorLevel.ansi256 color = TermColor.Color.ansi256Codes✝ layer color
• TermColor.Color.sgrCodes layer TermColor.ColorLevel.trueColor color = TermColor.Color.trueColorCodes✝ layer color

def TermColor.Style.sgrParameters (target : RenderTarget) (style : Style) : List Nat

The SGR parameter string for a style at a target capability.

Equations

• TermColor.Style.sgrParameters target style = if (!target.styles) = true then [] else List.flatMap (TermColor.Style.settingCodes✝ target) style.settings

def TermColor.Style.sgr (target : RenderTarget) (style : Style) : String

Encode a style as an SGR opening sequence.

Equations

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

def TermColor.Style.reset : String

Reset all SGR attributes and colors.

Equations

• TermColor.Style.reset = "\x1b[0m"

def TermColor.Style.wrap (target : RenderTarget) (style : Style) (text : String) : String

Wrap plain text in an opening SGR sequence and a complete reset.

Equations

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