0 | module Control.ANSI.CSI
  1 |
  2 | %default total
  3 |
  4 | ||| Moves the cursor n columns up.
  5 | ||| If the cursor is at the edge of the screen it has no effect.
  6 | export
  7 | cursorUp : Nat -> String
  8 | cursorUp n = "\x1B[" ++ show n ++ "A"
  9 |
 10 | export
 11 | cursorUp1 : String
 12 | cursorUp1 = cursorUp 1
 13 |
 14 | ||| Moves the cursor n columns down.
 15 | ||| If the cursor is at the edge of the screen it has no effect.
 16 | export
 17 | cursorDown : Nat -> String
 18 | cursorDown n = "\x1B[" ++ show n ++ "B"
 19 |
 20 | export
 21 | cursorDown1 : String
 22 | cursorDown1 = cursorDown 1
 23 |
 24 | ||| Moves the cursor n columns forward.
 25 | ||| If the cursor is at the edge of the screen it has no effect.
 26 | export
 27 | cursorForward : Nat -> String
 28 | cursorForward n = "\x1B[" ++ show n ++ "C"
 29 |
 30 | export
 31 | cursorForward1 : String
 32 | cursorForward1 = cursorForward 1
 33 |
 34 | ||| Moves the cursor n columns back.
 35 | ||| If the cursor is at the edge of the screen it has no effect.
 36 | export
 37 | cursorBack : Nat -> String
 38 | cursorBack n = "\x1B[" ++ show n ++ "D"
 39 |
 40 | export
 41 | cursorBack1 : String
 42 | cursorBack1 = cursorBack 1
 43 |
 44 | ||| Moves the cursor at the beginning of n lines down.
 45 | ||| If the cursor is at the edge of the screen it has no effect.
 46 | export
 47 | cursorNextLine : Nat -> String
 48 | cursorNextLine n = "\x1B[" ++ show n ++ "E"
 49 |
 50 | export
 51 | cursorNextLine1 : String
 52 | cursorNextLine1 = cursorNextLine 1
 53 |
 54 | ||| Moves the cursor at the beginning of n lines up.
 55 | ||| If the cursor is at the edge of the screen it has no effect.
 56 | export
 57 | cursorPrevLine : Nat -> String
 58 | cursorPrevLine n = "\x1B[" ++ show n ++ "F"
 59 |
 60 | export
 61 | cursorPrevLine1 : String
 62 | cursorPrevLine1 = cursorPrevLine 1
 63 |
 64 | ||| Moves the cursor at an arbitrary line and column.
 65 | ||| Both lines and columns start at 1.
 66 | export
 67 | cursorMove : (row : Nat) -> (col : Nat) -> String
 68 | cursorMove row col = "\x1B[" ++ show row ++ ";" ++ show col ++ "H"
 69 |
 70 | public export
 71 | data EraseDirection = Start | End | All
 72 |
 73 | Cast EraseDirection String where
 74 |   cast Start = "1"
 75 |   cast End = "0"
 76 |   cast All = "2"
 77 |
 78 | ||| Clears part of the screen.
 79 | export
 80 | eraseScreen : EraseDirection -> String
 81 | eraseScreen to = "\x1B[" ++ cast to ++ "J"
 82 |
 83 | ||| Clears part of the line.
 84 | export
 85 | eraseLine : EraseDirection -> String
 86 | eraseLine to = "\x1B[" ++ cast to ++ "K"
 87 |
 88 | ||| Scrolls the whole screen up by n lines.
 89 | export
 90 | scrollUp : Nat -> String
 91 | scrollUp n = "\x1B[" ++ show n ++ "S"
 92 |
 93 | export
 94 | scrollUp1 : String
 95 | scrollUp1 = scrollUp 1
 96 |
 97 | ||| Scrolls the whole screen down by n lines.
 98 | export
 99 | scrollDown : Nat -> String
100 | scrollDown n = "\x1B[" ++ show n ++ "T"
101 |
102 | export
103 | scrollDown1 : String
104 | scrollDown1 = scrollDown 1
105 |