Control.NCurses

Reexports

import public NCurses.Core.Color as Color
import public NCurses.Core.Input as Input
import public NCurses.Core.SpecialKey as SpecialKey
import public Control.NCurses.State

Definitions

0 NextIn : Window -> Type

Totality: total
Visibility: public export

data NCurses : Type -> CursesState -> CursesState -> Type

Totality: total
Visibility: export
Constructors:

Pure : a -> NCurses a s s

Bind : NCurses a s1 s2 -> (a -> NCurses b s2 s3) -> NCurses b s1 s3

Init : IsInactive s => NCurses () s initState

DeInit : IsActive s => NCurses () s Inactive

AddWindow : {auto {conArg:1262} : IsActive s} -> (name : String) -> Position -> Size -> Maybe (Exists (\c => (Border c, HasColor c s))) -> NCurses () s (addWindow s name)

SetWindow : IsActive s => (name : String) -> {auto {conArg:1293} : HasWindow name s} -> NCurses () s (setWindow s name)

UnsetWindow : IsActive s => {auto {conArg:1305} : HasWindow DefaultWindow s} -> NCurses () s (setWindow s DefaultWindow)

InWindow : IsActive s => (w : String) -> {auto {conArg:1318} : HasWindow w s} -> (IsActive (setWindow s w) => HasWindow w (setWindow s w) => InWindow w (setWindow s w) => NCurses () (setWindow s w) (setWindow s w)) -> NCurses () s s

AddColor : {auto {conArg:1348} : IsActive s} -> (name : String) -> Color -> Color -> NCurses () s (addColor s name)

ModAttr : IsActive s => AttrCmd s -> NCurses () s s

Clear : IsActive s => NCurses () s s

Erase : IsActive s => NCurses () s s

Refresh : IsActive s => NCurses () s s

RefreshAll : IsActive s => NCurses () s s

Output : IsActive s => OutputCmd s -> NCurses () s s

GetCursPos : IsActive s => NCurses Position s s

  Get the position of the cursor within the current window.

SetEcho : {auto {conArg:1413} : IsActive s} -> (on : Bool) -> NCurses () s (setEcho s on)

SetCBreak : {auto {conArg:1423} : IsActive s} -> (on : Bool) -> NCurses () s (setCBreak s on)

SetNoDelay : {auto {conArg:1433} : IsActive s} -> (on : Bool) -> NCurses () s (setNoDelay s on)

SetCursor : IsActive s => CursorVisibility -> NCurses () s s

SetKeypad : {auto {conArg:1454} : IsActive s} -> (on : Bool) -> NCurses () s (setKeypad s on)

GetWinPos : IsActive s => NCurses Position s s

  Get the position of the current window.

SetWinPos : IsActive s => Position -> NCurses () s s

  Set the position of the current window.

GetWinSize : IsActive s => Bool -> NCurses Size s s

  Get the size of the current window. If `internal` is @True@, then
  will subtract the space taken up by any border a window has.

SetWinSize : IsActive s => Size -> NCurses () s s

  Set thte size of the current window.

GetCh : {auto {conArg:1498} : IsActive s} -> NCurses (NextIn (currentWindow s)) s s

NIO : IO a -> NCurses a s s

Hints:

IndexedApplicative CursesState NCurses
IndexedFunctor CursesState CursesState NCurses
IndexedMonad CursesState NCurses

liftIO : IO a -> NCurses a s s

  Lift an arbitrary IO operation into NCurses.
  It's ill-advised to use stdout operations
  like `putStr` from `IO` while NCurses is
  active -- NCurses offers its own `putStr`
  and the standard terminal output will
  behave undesirably for the most part.

Totality: total
Visibility: export

init : IsInactive s => NCurses () s initState

  Initialize an NCurses session. While this session is active,
  normal terminal output will not behave the way you expect.

Totality: total
Visibility: export

deinit : IsActive s => NCurses () s Inactive

  End an NCurses session.

Totality: total
Visibility: export

addWindow : {auto {conArg:1882} : IsActive s} -> (name : String) -> Position -> Size -> Maybe (Exists (\c => (Border c, HasColor c s))) -> NCurses () s (addWindow s name)

  Add a window to the NCurses session.
  You get a default window encompassing the whole terminal screen, but
  adding windows gives finer control over clearing of parts of the screen,
  printing with coordinates relative to the smaller windows, etc.
  
  See the @border@ function for a convenient initializer of the @Border@ type.

Totality: total
Visibility: export

border : IsActive s => (color : String) -> HasColor color s => BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> BorderChar -> Maybe (Exists (\c => (Border c, HasColor c s)))

  Create a border for a window given the colors available in the current
  state.

Totality: total
Visibility: public export

defaultBorder : IsActive s => (color : String) -> HasColor color s => Maybe (Exists (\c => (Border c, HasColor c s)))

Totality: total
Visibility: public export

setWindow : IsActive s => (name : String) -> {auto {conArg:2004} : HasWindow name s} -> NCurses () s (setWindow s name)

  Set the current window. This is the window that future commands
  apply to (drawing, setting attributes, reading characters from).

Totality: total
Visibility: export

unsetWindow : IsActive s => {auto {conArg:2024} : HasWindow DefaultWindow s} -> NCurses () s (setWindow s DefaultWindow)

  Unset the current window. This results in the full screen (also known
  as the default or standard window) being "current."

Totality: total
Visibility: export

inWindow : IsActive s => (name : String) -> {auto {conArg:2048} : HasWindow name s} -> (IsActive (setWindow s name) => HasWindow name (setWindow s name) => InWindow name (setWindow s name) => NCurses () (setWindow s name) (setWindow s name)) -> NCurses () s s

  Perform some operations within another window, returning to the current window without
  modifying state afterwards.

Totality: total
Visibility: export

hasWindowWithin' : InWindow w s -> HasWindow w s

Totality: total
Visibility: public export

hasWindowWithin : InWindow w s => HasWindow w s

Totality: total
Visibility: public export

identifiesCurrentWindow : InWindow w (Active {_:2207} ws {_:2206} {_:2205}) => IdentifiesWindow w ws

Totality: total
Visibility: public export

setWindowHasWindowStill : HasWindow n s => {auto {conArg:2243} : HasWindow w s} -> HasWindow n (setWindow s w)

  If a given state has a window, setting a new current window on that state does not
  change the fact that the state has the original window.

Totality: total
Visibility: public export

setWindowIsActiveStill : IsActive s => {auto {conArg:2407} : HasWindow w s} -> IsActive (setWindow s w)

Totality: total
Visibility: public export

setWindowHasColorStill : HasColor c s => {auto {conArg:2442} : HasWindow w s} -> HasColor c (setWindow s w)

Totality: total
Visibility: public export

addWindowHasWindowStill : {auto {conArg:2536} : IsActive s} -> HasWindow n s => HasWindow n (addWindow s w)

  If a given state has a window, setting a new current window on that state does not
  change the fact that the state has the original window.

Totality: total
Visibility: public export

addWindowIsActiveStill : {auto {conArg:2641} : IsActive s} -> IsActive (addWindow s w)

Totality: total
Visibility: public export

addWindowHasColorStill : {auto {conArg:2664} : IsActive s} -> HasColor c s => HasColor c (addWindow s w)

Totality: total
Visibility: public export

identifiedWindowExists : ({arg:2755} : IdentifiesWindow w ws) -> Exists (\k => Exists (\d => lookupWindow w ws = MkWindow w k d))

Totality: total
Visibility: public export

inWindowNow : {auto {conArg:2814} : HasWindow w s} -> InWindow w (setWindow s w)

Totality: total
Visibility: public export

clear : IsActive s => NCurses () s s

  Clear the current window.
  
  Clearing tells NCurses to redraw the whole terminal on the next
  refresh. For a less intensive process that allows NCurses
  to determine what parts of the terminal need to be drawn,
  use @erase@.
  
  Clearing the standard window will require refreshing all
  windows after the next call to refresh the standard window,
  It probably makes sense much of the time to refresh immediately
  after a call to clear.

Totality: total
Visibility: export

erase : IsActive s => NCurses () s s

  Erase the current window.

Totality: total
Visibility: export

refresh : IsActive s => NCurses () s s

  Refresh the current window.

Totality: total
Visibility: export

refreshAll : IsActive s => NCurses () s s

  Refresh all windows.

Totality: total
Visibility: export

getPos : IsActive s => NCurses Position s s

  Get the position of the cursor within the current window.

Totality: total
Visibility: export

getWindowPos : IsActive s => NCurses Position s s

  Get the position of the current window.

Totality: total
Visibility: export

setWindowPos : IsActive s => Position -> NCurses () s s

  Set the position of the current window.

Totality: total
Visibility: export

getWindowSize : IsActive s => Bool -> NCurses Size s s

  Get the size of the current window.
  
  @ internal If @True@, the size will not include the space
             taken up by any internal border the window has
             applied to it. If @False@, the size will always
             be the space taken up by the window, not the space
             available inside the window.

Totality: total
Visibility: export

setWindowSize : IsActive s => Size -> NCurses () s s

  Set the size of the current window. If the window has a border,
  this size includes the single row & column taken up by the border
  on all sides.

Totality: total
Visibility: export

addColor : {auto {conArg:2994} : IsActive s} -> (name : String) -> Color -> Color -> NCurses () s (addColor s name)

  Add a color to the current NCurses session.
  
  Once added, colors can be referenced by name
  when constructing Attributes.

Totality: total
Visibility: export

enableAttr : IsActive s => Attribute s -> NCurses () s s

  Set the given attribute until it is set again.
  This has no impact on any other attributes that are set.
  
  In ncurses terminology, "attron"

Totality: total
Visibility: export

disableAttr : IsActive s => Attribute s -> NCurses () s s

  Unset the given attribute until it is set again.
  This has no impact on any other attributes that are set.
  
  In ncurses terminology, "attroff"

Totality: total
Visibility: export

setAttr : IsActive s => Attribute s -> NCurses () s s

  Set an attribute to be applied until it is cleared or
  overwritten. All other attributes are cleared at the same time.
  See @enabledAttr@ to enable an attribute without clearing other
  attributes.
  
  `setAttr Normal` clears all attributes.
  
  In ncurses terminology, "attrset"

Totality: total
Visibility: export

setAttrs : IsActive s => List (Attribute s) -> NCurses () s s

  Set all the given attributes, replacing any existing attributes.
  
  In ncurses terminology, "attrset"

Totality: total
Visibility: export

updateAttr : IsActive s => Attribute s -> ColorAttr s -> Maybe Nat -> NCurses () s s

  Update the attribute (only supports a single attribute for now) and color
  at the current position for the given length of characters. This allows
  you to change attributes of already printed characters.
  
  Specify a length of @Nothing@ to update the whole line.

Totality: total
Visibility: export

setBackground : IsActive s => ColorAttr s -> NCurses () s s

  Set the background color for the current window.

Totality: total
Visibility: export

putCh : IsActive s => Char -> NCurses () s s

  Print a character to the terminal.

Totality: total
Visibility: export

putStr : IsActive s => String -> NCurses () s s

  Print a string to the terminal _without_ a trailing newline.

Totality: total
Visibility: export

putStrLn : IsActive s => String -> NCurses () s s

  Print a string to the terminal _with_ a trailing newline.

Totality: total
Visibility: export

drawVerticalLine : IsActive s => Char -> Nat -> NCurses () s s

  Draw a vertical line to the current window comprised of the given
  character and having the given length.

Totality: total
Visibility: export

drawHorizontalLine : IsActive s => Char -> Nat -> NCurses () s s

  Draw a horizontal line to the current window comprised of the given
  character and having the given length.

Totality: total
Visibility: export

move : IsActive s => Position -> NCurses () s s

  Move the cursor to a position relative within the current window.
  
  If the window has a border, this position is _within_ the border.
  (0, 0) is the top left (row, column) without a border and with a
  border it is 1 row & column inset from there.

Totality: total
Visibility: export

setCBreak : {auto {conArg:3330} : IsActive s} -> (on : Bool) -> NCurses () s (setCBreak s on)

  cBreak indicates whether characters typed by the user are delivered to the
  program (via @getCh@) immediately or not. If not, they are delivered when a
  newline is typed (the default behavior for most terminal environments).
  
  This setting affects all windows.

Totality: total
Visibility: export

setEcho : {auto {conArg:3348} : IsActive s} -> (on : Bool) -> NCurses () s (setEcho s on)

  echo indicates whether characters typed by the user are printed to the screen
  by NCurses as well as delivered to @getCh@.
  
  This setting affects all windows.

Totality: total
Visibility: export

setKeypad : {auto {conArg:3366} : IsActive s} -> (on : Bool) -> NCurses () s (setKeypad s on)

  Turn "keypad" on or off.
  
  This property is set independently for each window. This method only sets the
  property for the current window.
  
  Set to true to receive "special keys" as single values rather than composites
  of two or more Chars. For example, arrow keys are represented as two input
  chars, but you will receive @Key@ values for them instead with the @keypad@
  property turned on.
  
  This is on by default.

Totality: total
Visibility: export

setNoDelay : {auto {conArg:3385} : IsActive s} -> (on : Bool) -> NCurses () s (setNoDelay s on)

  Turn "noDelay" on or off.
  
  This property is set independently for each window. This method only sets the
  property for the current window.
  
  This is off by default (i.e. by default @getInput@ waits for user input).

Totality: total
Visibility: export

setCursor : IsActive s => CursorVisibility -> NCurses () s s

  Set the way the cursor is displayed to the user.

Totality: total
Visibility: export

getInput : {auto {conArg:3421} : IsActive s} -> NCurses (NextIn (currentWindow s)) s s

  Get the next keypress or character input.
  
  If `noDelay` is turned on, @getInput@ returns immediately and results in
  @Nothing@ if the user has not typed anything. If `noDelay` is turned off,
  @getInput@ blocks until the user enters text. This will block until the next
  character is pressed by default, but if `cBreak` is turned off, it will block
  until the user inputs a newline (much like the default for most terminal input).
  
  If `keypad` is turned on, @getInput@ returns either a @Char@ or a @Key@ depending
  on whether the user has input one of the special-keys (like the arrow keys).

Totality: total
Visibility: export

getChar : IsActive s => NoKeypad s => YesDelay s => NCurses Char s s

Totality: total
Visibility: export

getChar : IsActive s => NoKeypad s => NoDelay s => NCurses (Maybe Char) s s

Totality: total
Visibility: export

getKeyOrChar : IsActive s => YesKeypad s => YesDelay s => NCurses (Either Char Key) s s

Totality: total
Visibility: export

getKeyOrChar : IsActive s => YesKeypad s => NoDelay s => NCurses (Maybe (Either Char Key)) s s

Totality: total
Visibility: export

keys : List (key, value) -> List key

Totality: total
Visibility: public export

withNCurses : HasIO io => NCurses a Inactive Inactive -> io a

  Run an NCurses program with guarantees
  that it is initialized at the beginning and
  deinitialied at the end.

Totality: total
Visibility: export