Idris.REPL.Common

Reexports

Definitions

iputStrLn : Ref Ctxt Defs => Ref ROpts REPLOpts => Doc IdrisAnn -> Core ()

  Output informational messages, unless suppressed by a flag.
  This function should only be called with informational
  messages, an unhandled error is an example of what should
  *not* end up here.

Visibility: export

data MsgStatus : Type

  Sampled against `VerbosityLvl`.

Totality: total
Visibility: public export
Constructors:

MsgStatusNone : MsgStatus

MsgStatusError : MsgStatus

MsgStatusInfo : MsgStatus

printResult : Ref ROpts REPLOpts => Doc IdrisAnn -> Core ()

  Print REPL result.

Visibility: export

printDocResult : Ref ROpts REPLOpts => Doc IdrisDocAnn -> Core ()

  Print REPL result.

Visibility: export

printError : Ref ROpts REPLOpts => Doc IdrisAnn -> Core ()

Visibility: export

emitProblem : Ref Ctxt Defs => Ref ROpts REPLOpts => Ref Syn SyntaxInfo => a -> DocCreator a -> DocCreator a -> (a -> Maybe FC) -> MsgStatus -> Core ()

Visibility: export

emitError : Ref Ctxt Defs => Ref ROpts REPLOpts => Ref Syn SyntaxInfo => Error -> Core ()

Visibility: export

emitWarning : Ref Ctxt Defs => Ref ROpts REPLOpts => Ref Syn SyntaxInfo => Warning -> Core ()

Visibility: export

emitWarnings : Ref Ctxt Defs => Ref ROpts REPLOpts => Ref Syn SyntaxInfo => Core (List Error)

Visibility: export

emitWarningsAndErrors : Ref Ctxt Defs => Ref ROpts REPLOpts => Ref Syn SyntaxInfo => List Error -> Core (List Error)

Visibility: export

updateErrorLine : Ref ROpts REPLOpts => List Error -> Core ()

Visibility: export

resetContext : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref MD Metadata => OriginDesc -> Core ()

Visibility: export

data EditResult : Type

Totality: total
Visibility: public export
Constructors:

DisplayEdit : Doc IdrisAnn -> EditResult

EditError : Doc IdrisAnn -> EditResult

MadeLemma : Maybe String -> Name -> IPTerm -> String -> EditResult

MadeWith : Maybe String -> List String -> EditResult

MadeCase : Maybe String -> List String -> EditResult

MadeIntro : List1 String -> EditResult

data MissedResult : Type

Totality: total
Visibility: public export
Constructors:

CasesMissing : Name -> List String -> MissedResult

CallsNonCovering : Name -> List Name -> MissedResult

AllCasesCovered : Name -> MissedResult

data REPLResult : Type

Totality: total
Visibility: public export
Constructors:

Done : REPLResult

REPLError : Doc IdrisAnn -> REPLResult

Executed : PTerm -> REPLResult

RequestedHelp : REPLResult

RequestedDetails : String -> REPLResult

Evaluated : IPTerm -> Maybe IPTerm -> REPLResult

Printed : Doc IdrisAnn -> REPLResult

PrintedDoc : Doc IdrisDocAnn -> REPLResult

TermChecked : IPTerm -> IPTerm -> REPLResult

FileLoaded : String -> REPLResult

ModuleLoaded : String -> REPLResult

ErrorLoadingModule : String -> Error -> REPLResult

ErrorLoadingFile : String -> FileError -> REPLResult

ErrorsBuildingFile : String -> List Error -> REPLResult

NoFileLoaded : REPLResult

CurrentDirectory : String -> REPLResult

CompilationFailed : REPLResult

Compiled : String -> REPLResult

ProofFound : IPTerm -> REPLResult

Missed : List MissedResult -> REPLResult

CheckedTotal : List (Name, Totality) -> REPLResult

OptionsSet : List REPLOpt -> REPLResult

LogLevelSet : Maybe LogLevel -> REPLResult

ConsoleWidthSet : Maybe Nat -> REPLResult

ColorSet : Bool -> REPLResult

VersionIs : Version -> REPLResult

DefDeclared : REPLResult

Exited : REPLResult

Edited : EditResult -> REPLResult

docsOrSignature : Ref ROpts REPLOpts => Ref Ctxt Defs => Ref Syn SyntaxInfo => FC -> Name -> Core (Doc IdrisDocAnn)

Visibility: export

equivTypes : Ref Ctxt Defs => ClosedTerm -> ClosedTerm -> Core Bool

Visibility: export