Idris2Doc : Hedgehog.Internal.Terminal

Hedgehog.Internal.Terminal

(source)
Definitions
interface HasTerminal : (Type -> Type) -> Type
  Interface showing that in the given monadic context `m` user can
  initialise terminal and use it for printing temporary and permanent info.

  Parameters: m
Methods:
  
0 TermTy : Type
  Type of initialised terminal
  
console : m TermTy
  Return new initialised terminal
  
  Notice that usage of several initalised terminals is not supposed
  and may lead to unexpected behaviour.
  
putTmp : TermTy -> String -> m ()
  Put temporary info into the terminal
  
  Any successive putting temporary or permanent info into the terminal
  makes any previously put temporary info disappear.
  
putOut : TermTy -> String -> m ()
  Put permanent info into the terminal
  
  This action makes previously put temporary info disappear

Implementation: 
HasIO io => HasTerminal io
0 TermTy : HasTerminal m => Type
  Type of initialised terminal

  Visibility: public export
console : {auto __con : HasTerminal m} -> m TermTy
  Return new initialised terminal
  
  Notice that usage of several initalised terminals is not supposed
  and may lead to unexpected behaviour.

  Visibility: public export
putTmp : {auto __con : HasTerminal m} -> TermTy -> String -> m ()
  Put temporary info into the terminal
  
  Any successive putting temporary or permanent info into the terminal
  makes any previously put temporary info disappear.

  Visibility: public export
putOut : {auto __con : HasTerminal m} -> TermTy -> String -> m ()
  Put permanent info into the terminal
  
  This action makes previously put temporary info disappear

  Visibility: public export
0 Terminal : (0 m : (Type -> Type)) -> HasTerminal m => Type
  Returns the type of initialised terminal
  for the explicitly given context `m`

  Visibility: public export
data StdoutOrTmp : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Stdout : StdoutOrTmp
  
Tmp : StdoutOrTmp