TermColor.Style: composable terminal styles

A style is a sequence of SGR settings. An attribute setting carries either true or false, so it can enable or disable a surrounding attribute; an absent setting means inherit. Settings are applied from left to right, and later settings therefore take precedence for overlapping properties. This is the same small algebra used by ANSI itself.

inductive TermColor.Attribute : Type

The text attributes represented by common SGR terminals.

• bold : Attribute

  Bold text.

• dim : Attribute

  Dim text.

• italic : Attribute

  Italic text.

• underline : Attribute

  Underlined text.

• blink : Attribute

  Blinking text.

• rapidBlink : Attribute

  Rapidly blinking text.

• reverse : Attribute

  Reversed foreground and background.

• conceal : Attribute

  Concealed text.

• strike : Attribute

  Struck-through text.

• doubleUnderline : Attribute

  Double-underlined text.

• framed : Attribute

  Framed text.

• encircled : Attribute

  Encircled text.

• overlined : Attribute

  Overlined text.

def TermColor.instBEqAttribute.beq : Attribute → Attribute → Bool

Equations

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

@[instance_reducible]

instance TermColor.instBEqAttribute : BEq Attribute

Equations

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

@[instance_reducible]

instance TermColor.instDecidableEqAttribute : DecidableEq Attribute

Equations

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

@[instance_reducible]

instance TermColor.instReprAttribute : Repr Attribute

Equations

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

def TermColor.instReprAttribute.repr : Attribute → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• TermColor.instReprAttribute.repr TermColor.Attribute.bold prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Attribute.bold")).group prec✝
• TermColor.instReprAttribute.repr TermColor.Attribute.dim prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Attribute.dim")).group prec✝
• TermColor.instReprAttribute.repr TermColor.Attribute.italic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Attribute.italic")).group prec✝
• TermColor.instReprAttribute.repr TermColor.Attribute.blink prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Attribute.blink")).group prec✝
• TermColor.instReprAttribute.repr TermColor.Attribute.strike prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Attribute.strike")).group prec✝
• TermColor.instReprAttribute.repr TermColor.Attribute.framed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TermColor.Attribute.framed")).group prec✝

inductive TermColor.Setting : Type

One setting in a style sequence.

• foreground : Color → Setting

  Set the foreground color.

• background : Color → Setting

  Set the background color.

• attr : Attribute → Bool → Setting

  Enable or disable an attribute.

@[instance_reducible]

instance TermColor.instBEqSetting : BEq Setting

Equations

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

def TermColor.instBEqSetting.beq : Setting → Setting → Bool

Equations

• TermColor.instBEqSetting.beq (TermColor.Setting.foreground a) (TermColor.Setting.foreground b) = (a == b)
• TermColor.instBEqSetting.beq (TermColor.Setting.background a) (TermColor.Setting.background b) = (a == b)
• TermColor.instBEqSetting.beq (TermColor.Setting.attr a a_1) (TermColor.Setting.attr b b_1) = (a == b && a_1 == b_1)
• TermColor.instBEqSetting.beq x✝¹ x✝ = false

@[instance_reducible]

instance TermColor.instDecidableEqSetting : DecidableEq Setting

Equations

• TermColor.instDecidableEqSetting = TermColor.instDecidableEqSetting.decEq

def TermColor.instDecidableEqSetting.decEq (x✝ x✝¹ : Setting) : Decidable (x✝ = x✝¹)

Equations

• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.foreground a) (TermColor.Setting.foreground b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.foreground a) (TermColor.Setting.background a_1) = isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.foreground a) (TermColor.Setting.attr a_1 a_2) = isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.background a) (TermColor.Setting.foreground a_1) = isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.background a) (TermColor.Setting.background b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.background a) (TermColor.Setting.attr a_1 a_2) = isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.attr a a_1) (TermColor.Setting.foreground a_2) = isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.attr a a_1) (TermColor.Setting.background a_2) = isFalse ⋯
• TermColor.instDecidableEqSetting.decEq (TermColor.Setting.attr a a_1) (TermColor.Setting.attr b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance TermColor.instReprSetting : Repr Setting

Equations

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

def TermColor.instReprSetting.repr : Setting → Nat → Std.Format

Equations

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

structure TermColor.Style : Type

A composable sequence of terminal settings.

• settings : List Setting

  Settings applied from left to right.

def TermColor.instBEqStyle.beq : Style → Style → Bool

Equations

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

@[instance_reducible]

instance TermColor.instBEqStyle : BEq Style

Equations

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

@[instance_reducible]

instance TermColor.instDecidableEqStyle : DecidableEq Style

Equations

• TermColor.instDecidableEqStyle = TermColor.instDecidableEqStyle.decEq

def TermColor.instDecidableEqStyle.decEq (x✝ x✝¹ : Style) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TermColor.instReprStyle : Repr Style

Equations

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

def TermColor.instReprStyle.repr : Style → Nat → Std.Format

Equations

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

def TermColor.Style.empty : Style

The empty style sequence.

Equations

• TermColor.Style.empty = { }

def TermColor.Style.combine (old new : Style) : Style

Concatenate style settings. Later settings are applied later by the terminal.

Equations

• old.combine new = { settings := old.settings ++ new.settings }

def TermColor.Style.«term_<+>_» : Lean.TrailingParserDescr

Combine styles, applying the right-hand settings after the left-hand settings.

Equations

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

def TermColor.Style.fg (color : Color) : Style

A foreground-color setting.

Equations

• TermColor.Style.fg color = { settings := [TermColor.Setting.foreground color] }

def TermColor.Style.bg (color : Color) : Style

A background-color setting.

Equations

• TermColor.Style.bg color = { settings := [TermColor.Setting.background color] }

def TermColor.Style.bold : Style

Turn one attribute on.

Equations

• TermColor.Style.bold = TermColor.Style.setAttribute✝ TermColor.Attribute.bold true

def TermColor.Style.dim : Style

Turn dim text on.

Equations

• TermColor.Style.dim = TermColor.Style.setAttribute✝ TermColor.Attribute.dim true

def TermColor.Style.italic : Style

Turn italic text on.

Equations

• TermColor.Style.italic = TermColor.Style.setAttribute✝ TermColor.Attribute.italic true

def TermColor.Style.underline : Style

Turn underlining on.

Equations

• TermColor.Style.underline = TermColor.Style.setAttribute✝ TermColor.Attribute.underline true

def TermColor.Style.blink : Style

Turn blinking on.

Equations

• TermColor.Style.blink = TermColor.Style.setAttribute✝ TermColor.Attribute.blink true

def TermColor.Style.rapidBlink : Style

Turn rapid blinking on.

Equations

• TermColor.Style.rapidBlink = TermColor.Style.setAttribute✝ TermColor.Attribute.rapidBlink true

def TermColor.Style.reverse : Style

Turn reverse video on.

Equations

• TermColor.Style.reverse = TermColor.Style.setAttribute✝ TermColor.Attribute.reverse true

def TermColor.Style.conceal : Style

Turn concealment on.

Equations

• TermColor.Style.conceal = TermColor.Style.setAttribute✝ TermColor.Attribute.conceal true

def TermColor.Style.strike : Style

Turn strike-through on.

Equations

• TermColor.Style.strike = TermColor.Style.setAttribute✝ TermColor.Attribute.strike true

def TermColor.Style.doubleUnderline : Style

Turn double underlining on.

Equations

• TermColor.Style.doubleUnderline = TermColor.Style.setAttribute✝ TermColor.Attribute.doubleUnderline true

def TermColor.Style.framed : Style

Turn framing on.

Equations

• TermColor.Style.framed = TermColor.Style.setAttribute✝ TermColor.Attribute.framed true

def TermColor.Style.encircled : Style

Turn encircling on.

Equations

• TermColor.Style.encircled = TermColor.Style.setAttribute✝ TermColor.Attribute.encircled true

def TermColor.Style.overlined : Style

Turn overlining on.

Equations

• TermColor.Style.overlined = TermColor.Style.setAttribute✝ TermColor.Attribute.overlined true

def TermColor.Style.notBold : Style

Turn one attribute off in an overlay.

Equations

• TermColor.Style.notBold = TermColor.Style.setAttribute✝ TermColor.Attribute.bold false

def TermColor.Style.notDim : Style

Turn dim text off in an overlay.

Equations

• TermColor.Style.notDim = TermColor.Style.setAttribute✝ TermColor.Attribute.dim false

def TermColor.Style.notItalic : Style

Turn italic text off in an overlay.

Equations

• TermColor.Style.notItalic = TermColor.Style.setAttribute✝ TermColor.Attribute.italic false

def TermColor.Style.notUnderline : Style

Turn underlining off in an overlay.

Equations

• TermColor.Style.notUnderline = TermColor.Style.setAttribute✝ TermColor.Attribute.underline false

def TermColor.Style.notBlink : Style

Turn blinking off in an overlay.

Equations

• TermColor.Style.notBlink = TermColor.Style.setAttribute✝ TermColor.Attribute.blink false

def TermColor.Style.notRapidBlink : Style

Turn rapid blinking off in an overlay.

Equations

• TermColor.Style.notRapidBlink = TermColor.Style.setAttribute✝ TermColor.Attribute.rapidBlink false

def TermColor.Style.notReverse : Style

Turn reverse video off in an overlay.

Equations

• TermColor.Style.notReverse = TermColor.Style.setAttribute✝ TermColor.Attribute.reverse false

def TermColor.Style.notConceal : Style

Turn concealment off in an overlay.

Equations

• TermColor.Style.notConceal = TermColor.Style.setAttribute✝ TermColor.Attribute.conceal false

def TermColor.Style.notStrike : Style

Turn strike-through off in an overlay.

Equations

• TermColor.Style.notStrike = TermColor.Style.setAttribute✝ TermColor.Attribute.strike false

def TermColor.Style.notDoubleUnderline : Style

Turn double underlining off in an overlay.

Equations

• TermColor.Style.notDoubleUnderline = TermColor.Style.setAttribute✝ TermColor.Attribute.doubleUnderline false

def TermColor.Style.notFramed : Style

Turn framing off in an overlay.

Equations

• TermColor.Style.notFramed = TermColor.Style.setAttribute✝ TermColor.Attribute.framed false

def TermColor.Style.notEncircled : Style

Turn encircling off in an overlay.

Equations

• TermColor.Style.notEncircled = TermColor.Style.setAttribute✝ TermColor.Attribute.encircled false

def TermColor.Style.notOverlined : Style

Turn overlining off in an overlay.

Equations

• TermColor.Style.notOverlined = TermColor.Style.setAttribute✝ TermColor.Attribute.overlined false

def TermColor.Style.black : Style

A black foreground style.

Equations

• TermColor.Style.black = TermColor.Style.fg TermColor.Color.black

def TermColor.Style.red : Style

A red foreground style.

Equations

• TermColor.Style.red = TermColor.Style.fg TermColor.Color.red

def TermColor.Style.green : Style

A green foreground style.

Equations

• TermColor.Style.green = TermColor.Style.fg TermColor.Color.green

def TermColor.Style.yellow : Style

A yellow foreground style.

Equations

• TermColor.Style.yellow = TermColor.Style.fg TermColor.Color.yellow

def TermColor.Style.blue : Style

A blue foreground style.

Equations

• TermColor.Style.blue = TermColor.Style.fg TermColor.Color.blue

def TermColor.Style.magenta : Style

A magenta foreground style.

Equations

• TermColor.Style.magenta = TermColor.Style.fg TermColor.Color.magenta

def TermColor.Style.cyan : Style

A cyan foreground style.

Equations

• TermColor.Style.cyan = TermColor.Style.fg TermColor.Color.cyan

def TermColor.Style.white : Style

A white foreground style.

Equations

• TermColor.Style.white = TermColor.Style.fg TermColor.Color.white

def TermColor.Style.onBlack : Style

A black background style.

Equations

• TermColor.Style.onBlack = TermColor.Style.bg TermColor.Color.black

def TermColor.Style.onRed : Style

A red background style.

Equations

• TermColor.Style.onRed = TermColor.Style.bg TermColor.Color.red

def TermColor.Style.onGreen : Style

A green background style.

Equations

• TermColor.Style.onGreen = TermColor.Style.bg TermColor.Color.green

def TermColor.Style.onYellow : Style

A yellow background style.

Equations

• TermColor.Style.onYellow = TermColor.Style.bg TermColor.Color.yellow

def TermColor.Style.onBlue : Style

A blue background style.

Equations

• TermColor.Style.onBlue = TermColor.Style.bg TermColor.Color.blue

def TermColor.Style.onMagenta : Style

A magenta background style.

Equations

• TermColor.Style.onMagenta = TermColor.Style.bg TermColor.Color.magenta

def TermColor.Style.onCyan : Style

A cyan background style.

Equations

• TermColor.Style.onCyan = TermColor.Style.bg TermColor.Color.cyan

def TermColor.Style.onWhite : Style

A white background style.

Equations

• TermColor.Style.onWhite = TermColor.Style.bg TermColor.Color.white