------------------------------------------------------------------------
-- 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 ∷ [])
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4