Idris.REPL

Reexports

Definitions

execExp : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => PTerm -> Core REPLResult

Visibility: export

compileExp : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => PTerm -> String -> Core REPLResult

Visibility: export

loadMainFile : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => String -> Core REPLResult

Visibility: export

process : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => REPLCmd -> Core REPLResult

  Process a single `REPLCmd`
  
  Returns `REPLResult` for display by the higher level shell which
  is invoking this interactive command processing.

Visibility: export

parseRepl : String -> Either Error (Maybe REPLCmd)

Visibility: export

interpret : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => String -> Core REPLResult

Visibility: export

replCmd : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => String -> Core ()

Visibility: export

repl : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => Core ()

Visibility: export

handleMissing' : MissedResult -> String

Visibility: export

handleMissing : MissedResult -> Doc IdrisAnn

Visibility: export

handleResult : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts => REPLResult -> Core ()

Visibility: export

displayResult : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => REPLResult -> Core ()

Visibility: export

displayHelp : String

Visibility: export

displayStartupErrors : Ref ROpts REPLOpts => REPLResult -> Core ()

  Display errors that may occur when starting the REPL.
  Does not force the REPL to exit, just prints the error(s).
  
  NOTE: functionally the only reason to consider this function specialized
  to "startup" is that it will provide suggestions to the user under the
  assumption that the user has just entered the REPL via CLI arguments that
  they may have used incorrectly.

Visibility: export