Idris2Doc : Idris.REPL.Opts

Idris.REPL.Opts

(source)
Definitions
data VerbosityLvl : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NoneLvl : VerbosityLvl
  Suppress all message output to `stdout`.
  
ErrorLvl : VerbosityLvl
  Keep only errors.
  
InfoLvl : VerbosityLvl
  Keep everything.
data OutputMode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
IDEMode : Integer -> File -> File -> OutputMode
  
REPL : VerbosityLvl -> OutputMode
  Given that we can divide elaboration messages into
  two categories: informational message and error message,
  `VerbosityLvl` applies a filter on the output,
   suppressing writes to `stdout` if the level condition isn't met.
record REPLOpts : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkREPLOpts : Bool -> REPLEval -> Bool -> Maybe String -> Maybe LiterateStyle -> String -> String -> Maybe Int -> OutputMode -> String -> Maybe (Name, Core (Search RawImp)) -> Maybe (Int, Core (Search (FC, List ImpClause))) -> Maybe Name -> List (String, Codegen) -> Maybe Nat -> Bool -> Bool -> REPLOpts

  Projections:
  
.color : REPLOpts -> Bool
  
.consoleWidth : REPLOpts -> Maybe Nat
  
.currentElabSource : REPLOpts -> String
  
.editor : REPLOpts -> String
  
.errorLine : REPLOpts -> Maybe Int
  
.evalMode : REPLOpts -> REPLEval
  
.evalResultName : REPLOpts -> Maybe Name
  
.evalTiming : REPLOpts -> Bool
  
.extraCodegens : REPLOpts -> List (String, Codegen)
  
.gdResult : REPLOpts -> Maybe (Int, Core (Search (FC, List ImpClause)))
  
.idemode : REPLOpts -> OutputMode
  
.literateStyle : REPLOpts -> Maybe LiterateStyle
  
.mainfile : REPLOpts -> Maybe String
  
.psResult : REPLOpts -> Maybe (Name, Core (Search RawImp))
  
.showTypes : REPLOpts -> Bool
  
.source : REPLOpts -> String
  
.synHighlightOn : REPLOpts -> Bool
.showTypes : REPLOpts -> Bool
  Totality: total
  Visibility: public export
showTypes : REPLOpts -> Bool
  Totality: total
  Visibility: public export
.evalMode : REPLOpts -> REPLEval
  Totality: total
  Visibility: public export
evalMode : REPLOpts -> REPLEval
  Totality: total
  Visibility: public export
.evalTiming : REPLOpts -> Bool
  Totality: total
  Visibility: public export
evalTiming : REPLOpts -> Bool
  Totality: total
  Visibility: public export
.mainfile : REPLOpts -> Maybe String
  Totality: total
  Visibility: public export
mainfile : REPLOpts -> Maybe String
  Totality: total
  Visibility: public export
.literateStyle : REPLOpts -> Maybe LiterateStyle
  Totality: total
  Visibility: public export
literateStyle : REPLOpts -> Maybe LiterateStyle
  Totality: total
  Visibility: public export
.source : REPLOpts -> String
  Totality: total
  Visibility: public export
source : REPLOpts -> String
  Totality: total
  Visibility: public export
.editor : REPLOpts -> String
  Totality: total
  Visibility: public export
editor : REPLOpts -> String
  Totality: total
  Visibility: public export
.errorLine : REPLOpts -> Maybe Int
  Totality: total
  Visibility: public export
errorLine : REPLOpts -> Maybe Int
  Totality: total
  Visibility: public export
.idemode : REPLOpts -> OutputMode
  Totality: total
  Visibility: public export
idemode : REPLOpts -> OutputMode
  Totality: total
  Visibility: public export
.currentElabSource : REPLOpts -> String
  Totality: total
  Visibility: public export
currentElabSource : REPLOpts -> String
  Totality: total
  Visibility: public export
.psResult : REPLOpts -> Maybe (Name, Core (Search RawImp))
  Totality: total
  Visibility: public export
psResult : REPLOpts -> Maybe (Name, Core (Search RawImp))
  Totality: total
  Visibility: public export
.gdResult : REPLOpts -> Maybe (Int, Core (Search (FC, List ImpClause)))
  Totality: total
  Visibility: public export
gdResult : REPLOpts -> Maybe (Int, Core (Search (FC, List ImpClause)))
  Totality: total
  Visibility: public export
.evalResultName : REPLOpts -> Maybe Name
  Totality: total
  Visibility: public export
evalResultName : REPLOpts -> Maybe Name
  Totality: total
  Visibility: public export
.extraCodegens : REPLOpts -> List (String, Codegen)
  Totality: total
  Visibility: public export
extraCodegens : REPLOpts -> List (String, Codegen)
  Totality: total
  Visibility: public export
.consoleWidth : REPLOpts -> Maybe Nat
  Totality: total
  Visibility: public export
consoleWidth : REPLOpts -> Maybe Nat
  Totality: total
  Visibility: public export
.color : REPLOpts -> Bool
  Totality: total
  Visibility: public export
color : REPLOpts -> Bool
  Totality: total
  Visibility: public export
.synHighlightOn : REPLOpts -> Bool
  Totality: total
  Visibility: public export
synHighlightOn : REPLOpts -> Bool
  Totality: total
  Visibility: public export
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
  Visibility: export
data ROpts : Type
  Totality: total
  Visibility: export
withROpts : Ref ROpts REPLOpts => Core a -> Core a
  Totality: total
  Visibility: export
setOutput : Ref ROpts REPLOpts => OutputMode -> Core ()
  Totality: total
  Visibility: export
getOutput : Ref ROpts REPLOpts => Core OutputMode
  Totality: total
  Visibility: export
setMainFile : Ref ROpts REPLOpts => Maybe String -> Core ()
  Totality: total
  Visibility: export
resetProofState : Ref ROpts REPLOpts => Core ()
  Visibility: export
setSource : Ref ROpts REPLOpts => String -> Core ()
  Totality: total
  Visibility: export
getSource : Ref ROpts REPLOpts => Core String
  Totality: total
  Visibility: export
getSourceLine : Ref ROpts REPLOpts => Int -> Core (Maybe String)
  Totality: total
  Visibility: export
getLitStyle : Ref ROpts REPLOpts => Core (Maybe LiterateStyle)
  Totality: total
  Visibility: export
setCurrentElabSource : Ref ROpts REPLOpts => String -> Core ()
  Totality: total
  Visibility: export
getCurrentElabSource : Ref ROpts REPLOpts => Core String
  Totality: total
  Visibility: export
getCodegen : Ref ROpts REPLOpts => String -> Core (Maybe Codegen)
  Totality: total
  Visibility: export
getConsoleWidth : Ref ROpts REPLOpts => Core (Maybe Nat)
  Totality: total
  Visibility: export
setConsoleWidth : Ref ROpts REPLOpts => Maybe Nat -> Core ()
  Totality: total
  Visibility: export
getColor : Ref ROpts REPLOpts => Core Bool
  Totality: total
  Visibility: export
setColor : Ref ROpts REPLOpts => Bool -> Core ()
  Totality: total
  Visibility: export
getSynHighlightOn : Ref ROpts REPLOpts => Core Bool
  Totality: total
  Visibility: export
setSynHighlightOn : Ref ROpts REPLOpts => Bool -> Core ()
  Totality: total
  Visibility: export
getEvalTiming : Ref ROpts REPLOpts => Core Bool
  Totality: total
  Visibility: export
setEvalTiming : Ref ROpts REPLOpts => Bool -> Core ()
  Totality: total
  Visibility: export