std.terminal

For the terminal the program runs on, console: whether it has one (interactive), its size (measure), the keys typed at it one at a time (readInput; not a line at a time, nor shown as they are typed: raw, begin to finish), and a screen drawn on it (draw). The C backend’s alone; what is drawn and what the keys are is std.terminal.widget’s, pure. Import it by a name, import std.terminal as Terminal.

import co
import std.terminal as Terminal
import std.terminal.widget as Widget

-- | a number, up and down by the arrows, until `q`
counter : Widget.App Int Int
counter =
  { start = 0
  , step = \k n -> case k of
      ArrowUp -> Continue (n + 1)
      ArrowDown -> Continue (n - 1)
      Char 'q' -> Done n
      _ -> Continue n
  , view = \size n ->
      { rows = [[Widget.bold (debug n)], Widget.status size.columns "↑↓  q quits"]
      , cursor = Nothing
      }
  }

-- | >>> Widget.shownAfter counter { columns = 12, rows = 2 } [ArrowUp, ArrowUp]
-- | ["2", "↑↓  q quits "]
counted : {e : HFunctor} -> {{con : Terminal.console <: e}} -> Co e (Maybe Int)
counted = Terminal.interact counter

interact runs an app of std.terminal.widget’s there: the terminal made raw, the app drawn on a screen of its own (the alternate one, which a terminal keeps apart from what was written before), each key stepped and the app drawn again, until it is done — then the terminal as it was, what was written before shown again. It gives Just what the app came to, or Nothing if there is no terminal or the input ended. The terminal is put back as it was however the program ends: at its end, at a failure, and where it is ended by a signal (Ctrl-C’s, SIGTERM, SIGHUP); Ctrl-Z puts it back while the program is stopped, and raw again, and the app drawn again, when it goes on, as a change of the terminal’s size does.

ConsoleF

data ConsoleF (m : Type -> Type) x
  = Interactive (Bool -> x)
  | Begin (Bool -> x)
  | Finish x
  | Measure (Widget.Size -> x)
  | ReadInput (Maybe String -> x)
  | Draw String x

console

console : HFunctor

For an interactive terminal: whether there is one, a session on it begun and finished, its size, input read, the screen drawn.

interactive

interactive : {e : HFunctor} -> {{ev : console <: e}} -> Co e Bool

The program’s standard input and output are a terminal, one an app may be drawn on: TERM is not dumb (on Windows, never yet).

begin

begin : {e : HFunctor} -> {{ev : console <: e}} -> Co e Bool

The terminal made raw — each key read as it is typed, not shown — and a screen of its own shown, empty: whether it could be.

finish

finish : {e : HFunctor} -> {{ev : console <: e}} -> Co e Unit

The terminal as it was before begin, what was written before shown again.

measure

measure : {e : HFunctor} -> {{ev : console <: e}} -> Co e Widget.Size

The terminal’s size, in columns and rows (80 by 24 where it does not say).

readInput

readInput : {e : HFunctor} -> {{ev : console <: e}} -> Co e (Maybe String)

What is typed next, as it comes, waited for: a key, or a few typed at once (Widget.decode reads them); Just "" where the terminal changed its size, or the program went on after it was stopped, so that what is shown is drawn again; Nothing at the end of the input.

draw

draw : {e : HFunctor} -> {{ev : console <: e}} -> String -> Co e Unit

Text written to the terminal as it is: what draws a screen (Widget.paint).

loop

loop : {e : HFunctor}
     -> {{ev : console <: e}}
     -> {s r : Type}
     -> (s -> Co e s)
     -> Widget.App s r
     -> s
     -> Co e (Maybe r)

interactWith

interactWith : {e : HFunctor}
             -> {{ev : console <: e}}
             -> {s r : Type}
             -> (s -> Co e s)
             -> Widget.App s r
             -> Co e (Maybe r)

The app run on the terminal, as above, each state it comes to given first to look, for what the app shows that is found in the world (the files a path typed completes to, std.cli.interactive’s listed): what it came to; Nothing where there is no terminal to run it on, or its input ended first.

interact

interact : {e : HFunctor}
         -> {{ev : console <: e}}
         -> {s r : Type}
         -> Widget.App s r
         -> Co e (Maybe r)

The app run on the terminal, as above, nothing looked at.