Libraries.Control.ANSI.CSI

Definitions

cursorUp : Nat -> String

  Moves the cursor n columns up.
  If the cursor is at the edge of the screen it has no effect.

Totality: total
Visibility: export

cursorUp1 : String

Totality: total
Visibility: export

cursorDown : Nat -> String

  Moves the cursor n columns down.
  If the cursor is at the edge of the screen it has no effect.

Totality: total
Visibility: export

cursorDown1 : String

Totality: total
Visibility: export

cursorForward : Nat -> String

  Moves the cursor n columns forward.
  If the cursor is at the edge of the screen it has no effect.

Totality: total
Visibility: export

cursorForward1 : String

Totality: total
Visibility: export

cursorBack : Nat -> String

  Moves the cursor n columns back.
  If the cursor is at the edge of the screen it has no effect.

Totality: total
Visibility: export

cursorBack1 : String

Totality: total
Visibility: export

cursorNextLine : Nat -> String

  Moves the cursor at the beginning of n lines down.
  If the cursor is at the edge of the screen it has no effect.

Totality: total
Visibility: export

cursorNextLine1 : String

Totality: total
Visibility: export

cursorPrevLine : Nat -> String

  Moves the cursor at the beginning of n lines up.
  If the cursor is at the edge of the screen it has no effect.

Totality: total
Visibility: export

cursorPrevLine1 : String

Totality: total
Visibility: export

cursorMove : Nat -> Nat -> String

  Moves the cursor at an arbitrary line and column.
  Both lines and columns start at 1.

Totality: total
Visibility: export

data EraseDirection : Type

Totality: total
Visibility: public export
Constructors:

Start : EraseDirection

End : EraseDirection

All : EraseDirection

Hint: 

Cast EraseDirection String

eraseScreen : EraseDirection -> String

  Clears part of the screen.

Totality: total
Visibility: export

eraseLine : EraseDirection -> String

  Clears part of the line.

Totality: total
Visibility: export

scrollUp : Nat -> String

  Scrolls the whole screen up by n lines.

Totality: total
Visibility: export

scrollUp1 : String

Totality: total
Visibility: export

scrollDown : Nat -> String

  Scrolls the whole screen down by n lines.

Totality: total
Visibility: export

scrollDown1 : String

Totality: total
Visibility: export