mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
Merge pull request #370 from ShinKage/ansi
Adds ANSI codes support in contrib
This commit is contained in:
commit
53621f84c5
@ -34,6 +34,8 @@ Library changes:
|
||||
* Added `Control.Monad.ST`, for update in-place via `STRef` (which is like
|
||||
`IORef`, but can escape from `IO`). Also added `Data.Ref` which provides an
|
||||
interface to both `IORef` and `STRef`.
|
||||
* Added `Control.ANSI` in `contrib`, for usage of ANSI escape codes for text
|
||||
styling and cursor/screen control in terminals.
|
||||
|
||||
Command-line options changes:
|
||||
|
||||
|
36
libs/contrib/Control/ANSI.idr
Normal file
36
libs/contrib/Control/ANSI.idr
Normal file
@ -0,0 +1,36 @@
|
||||
module Control.ANSI
|
||||
|
||||
import public Control.ANSI.CSI
|
||||
import public Control.ANSI.SGR
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
record DecoratedString where
|
||||
constructor MkDString
|
||||
sgr : List SGR
|
||||
str : String
|
||||
|
||||
export
|
||||
Show DecoratedString where
|
||||
show dstr = escapeSGR dstr.sgr ++ dstr.str ++ escapeSGR [Reset]
|
||||
|
||||
export
|
||||
colored : Color -> String -> DecoratedString
|
||||
colored c = MkDString [SetForeground c]
|
||||
|
||||
export
|
||||
background : Color -> String -> DecoratedString
|
||||
background c = MkDString [SetBackground c]
|
||||
|
||||
export
|
||||
bolden : String -> DecoratedString
|
||||
bolden = MkDString [SetStyle Bold]
|
||||
|
||||
export
|
||||
italicize : String -> DecoratedString
|
||||
italicize = MkDString [SetStyle Italic]
|
||||
|
||||
export
|
||||
underline : String -> DecoratedString
|
||||
underline = MkDString [SetStyle SingleUnderline]
|
105
libs/contrib/Control/ANSI/CSI.idr
Normal file
105
libs/contrib/Control/ANSI/CSI.idr
Normal file
@ -0,0 +1,105 @@
|
||||
module Control.ANSI.CSI
|
||||
|
||||
%default total
|
||||
|
||||
||| Moves the cursor n columns up.
|
||||
||| If the cursor is at the edge of the screen it has no effect.
|
||||
export
|
||||
cursorUp : Nat -> String
|
||||
cursorUp n = "\x1B[" ++ show n ++ "A"
|
||||
|
||||
export
|
||||
cursorUp1 : String
|
||||
cursorUp1 = cursorUp 1
|
||||
|
||||
||| Moves the cursor n columns down.
|
||||
||| If the cursor is at the edge of the screen it has no effect.
|
||||
export
|
||||
cursorDown : Nat -> String
|
||||
cursorDown n = "\x1B[" ++ show n ++ "B"
|
||||
|
||||
export
|
||||
cursorDown1 : String
|
||||
cursorDown1 = cursorDown 1
|
||||
|
||||
||| Moves the cursor n columns forward.
|
||||
||| If the cursor is at the edge of the screen it has no effect.
|
||||
export
|
||||
cursorForward : Nat -> String
|
||||
cursorForward n = "\x1B[" ++ show n ++ "C"
|
||||
|
||||
export
|
||||
cursorForward1 : String
|
||||
cursorForward1 = cursorForward 1
|
||||
|
||||
||| Moves the cursor n columns back.
|
||||
||| If the cursor is at the edge of the screen it has no effect.
|
||||
export
|
||||
cursorBack : Nat -> String
|
||||
cursorBack n = "\x1B[" ++ show n ++ "D"
|
||||
|
||||
export
|
||||
cursorBack1 : String
|
||||
cursorBack1 = cursorBack 1
|
||||
|
||||
||| Moves the cursor at the beginning of n lines down.
|
||||
||| If the cursor is at the edge of the screen it has no effect.
|
||||
export
|
||||
cursorNextLine : Nat -> String
|
||||
cursorNextLine n = "\x1B[" ++ show n ++ "E"
|
||||
|
||||
export
|
||||
cursorNextLine1 : String
|
||||
cursorNextLine1 = cursorNextLine 1
|
||||
|
||||
||| Moves the cursor at the beginning of n lines up.
|
||||
||| If the cursor is at the edge of the screen it has no effect.
|
||||
export
|
||||
cursorPrevLine : Nat -> String
|
||||
cursorPrevLine n = "\x1B[" ++ show n ++ "F"
|
||||
|
||||
export
|
||||
cursorPrevLine1 : String
|
||||
cursorPrevLine1 = cursorPrevLine 1
|
||||
|
||||
||| Moves the cursor at an arbitrary line and column.
|
||||
||| Both lines and columns start at 1.
|
||||
export
|
||||
cursorMove : (row : Nat) -> (col : Nat) -> String
|
||||
cursorMove row col = "\x1B[" ++ show row ++ ";" ++ show col ++ "H"
|
||||
|
||||
public export
|
||||
data EraseDirection = Start | End | All
|
||||
|
||||
Cast EraseDirection String where
|
||||
cast Start = "1"
|
||||
cast End = "0"
|
||||
cast All = "2"
|
||||
|
||||
||| Clears part of the screen.
|
||||
export
|
||||
eraseScreen : EraseDirection -> String
|
||||
eraseScreen to = "\x1B[" ++ cast to ++ "J"
|
||||
|
||||
||| Clears part of the line.
|
||||
export
|
||||
eraseLine : EraseDirection -> String
|
||||
eraseLine to = "\x1B[" ++ cast to ++ "K"
|
||||
|
||||
||| Scrolls the whole screen up by n lines.
|
||||
export
|
||||
scrollUp : Nat -> String
|
||||
scrollUp n = "\x1B[" ++ show n ++ "S"
|
||||
|
||||
export
|
||||
scrollUp1 : String
|
||||
scrollUp1 = scrollUp 1
|
||||
|
||||
||| Scrolls the whole screen down by n lines.
|
||||
export
|
||||
scrollDown : Nat -> String
|
||||
scrollDown n = "\x1B[" ++ show n ++ "T"
|
||||
|
||||
export
|
||||
scrollDown1 : String
|
||||
scrollDown1 = scrollDown 1
|
73
libs/contrib/Control/ANSI/SGR.idr
Normal file
73
libs/contrib/Control/ANSI/SGR.idr
Normal file
@ -0,0 +1,73 @@
|
||||
module Control.ANSI.SGR
|
||||
|
||||
import Data.List
|
||||
|
||||
%default total
|
||||
|
||||
public export
|
||||
data Color
|
||||
= Black | Red | Green | Yellow | Blue | Magenta | Cyan | White
|
||||
| BrightBlack | BrightRed | BrightGreen | BrightYellow | BrightBlue | BrightMagenta | BrightCyan | BrightWhite
|
||||
|
||||
Cast Color String where
|
||||
cast Black = "0"
|
||||
cast Red = "1"
|
||||
cast Green = "2"
|
||||
cast Yellow = "3"
|
||||
cast Blue = "4"
|
||||
cast Magenta = "5"
|
||||
cast Cyan = "6"
|
||||
cast White = "7"
|
||||
cast BrightBlack = "8"
|
||||
cast BrightRed = "9"
|
||||
cast BrightGreen = "10"
|
||||
cast BrightYellow = "11"
|
||||
cast BrightBlue = "12"
|
||||
cast BrightMagenta = "13"
|
||||
cast BrightCyan = "14"
|
||||
cast BrightWhite = "15"
|
||||
|
||||
public export
|
||||
data Style
|
||||
= Bold | Faint | NotBoldOrFaint | Italic
|
||||
| SingleUnderline | DoubleUnderline | NoUnderline
|
||||
| Striked | NotStriked
|
||||
|
||||
Cast Style String where
|
||||
cast Bold = "1"
|
||||
cast Faint = "2"
|
||||
cast NotBoldOrFaint = "22"
|
||||
cast Italic = "3"
|
||||
cast SingleUnderline = "4"
|
||||
cast DoubleUnderline = "21"
|
||||
cast NoUnderline = "24"
|
||||
cast Striked = "9"
|
||||
cast NotStriked = "29"
|
||||
|
||||
public export
|
||||
data Blink = Slow | Rapid | NoBlink
|
||||
|
||||
Cast Blink String where
|
||||
cast Slow = "5"
|
||||
cast Rapid = "6"
|
||||
cast NoBlink = "25"
|
||||
|
||||
public export
|
||||
data SGR
|
||||
= Reset
|
||||
| SetForeground Color
|
||||
| SetBackground Color
|
||||
| SetStyle Style
|
||||
| SetBlink Blink
|
||||
|
||||
||| Returns the ANSI escape code equivalent to the list of operations provided.
|
||||
export
|
||||
escapeSGR : List SGR -> String
|
||||
escapeSGR xs = "\x1B[" ++ concat (intersperse ";" (toCode <$> xs)) ++ "m"
|
||||
where
|
||||
toCode : SGR -> String
|
||||
toCode Reset = "0"
|
||||
toCode (SetForeground c) = "38;5;" ++ cast c
|
||||
toCode (SetBackground c) = "48;5;" ++ cast c
|
||||
toCode (SetStyle s) = cast s
|
||||
toCode (SetBlink b) = cast b
|
@ -1,6 +1,9 @@
|
||||
package contrib
|
||||
|
||||
modules = Control.Delayed,
|
||||
modules = Control.ANSI,
|
||||
Control.ANSI.SGR,
|
||||
Control.ANSI.CSI,
|
||||
Control.Delayed,
|
||||
Control.Linear.LIO,
|
||||
Control.Monad.Syntax,
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user