    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- ANSI escape codes
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module System.Console.ANSI where

    open import Data.List.Base as List using (List; []; _∷_)
    open import Data.Nat.Base using (ℕ; _+_)
    import Data.Nat.Show as ℕ using (show)
    open import Data.String.Base using (String; concat; intersperse)
    open import Function.Base using (_$_; case_of_)

    data Layer : Set where
      foreground background : Layer

    data Colour : Set where
      black red green yellow blue magenta cyan white : Colour

    data Intensity : Set where
      classic bright : Intensity

    data Weight : Set where
      bold faint normal : Weight

    data Underlining : Set where
      single double : Underlining

    data Style : Set where
      italic straight : Style

    data Blinking : Set where
      slow rapid : Blinking

    data Command : Set where
      reset : Command
      setColour : Layer → Intensity → Colour → Command
      setWeight : Weight → Command
      setStyle : Style → Command
      setUnderline : Underlining → Command
      setBlinking : Blinking → Command

    private

      escape : String → String
      escape txt = concat $ "\x1b[" ∷ txt ∷ "m" ∷ []

    encode : Command → String
    encode reset = "0"
    encode (setColour l i c) = ℕ.show (layer l + colour c + intensity i)

      where

      layer : Layer → ℕ
      layer foreground = 30
      layer background = 40

      colour : Colour → ℕ
      colour black   = 0
      colour red     = 1
      colour green   = 2
      colour yellow  = 3
      colour blue    = 4
      colour magenta = 5
      colour cyan    = 6
      colour white   = 7

      intensity : Intensity → ℕ
      intensity classic = 0
      intensity bright  = 60

    encode (setWeight w) = case w of λ where
      bold   → "1"
      faint  → "2"
      normal → "22"

    encode (setStyle s) = case s of λ where
      italic → "3"
      straight → "23"

    encode (setUnderline i) = case i of λ where
      single → "4"
      double → "21"

    encode (setBlinking b) = case b of λ where
      slow → "5"
      rapid → "6"

    command : Command → String
    command c = escape (encode c)

    withCommand : Command → String → String
    withCommand c txt = concat (command c ∷ txt ∷ command reset ∷ [])

    commands : List Command → String
    commands [] = command reset
    commands cs = escape (intersperse ";" $ List.map encode cs)

    withCommands : List Command → String → String
    withCommands cs txt = concat (commands cs ∷ txt ∷ command reset ∷ [])