diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 91e098ed55..f03ca31b3d 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -351,6 +351,8 @@ displayIDEResult outf i (REPL $ NoFileLoaded) = printIDEError outf i $ reflow "No file can be reloaded" displayIDEResult outf i (REPL $ CurrentDirectory dir) = printIDEResult outf i $ AString $ "Current working directory is \"\{dir}\"" +displayIDEResult outf i (REPL CompilationFailed) + = printIDEError outf i $ reflow "Compilation failed" displayIDEResult outf i (REPL $ Compiled f) = printIDEResult outf i $ AString "File \{f} written" displayIDEResult outf i (REPL $ ProofFound x) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 5eca1d8ef0..4282d2fc4d 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -1260,6 +1260,7 @@ mutual displayResult NoFileLoaded = printResult (reflow "No file can be reloaded") displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> dquotes (pretty0 dir)) + displayResult CompilationFailed = printResult (reflow "Compilation failed") displayResult (Compiled f) = printResult ("File" <++> pretty0 f <++> "written") displayResult (ProofFound x) = printResult (prettyBy Syntax x) displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases) diff --git a/src/Idris/REPL/Common.idr b/src/Idris/REPL/Common.idr index b91284507c..4d58b20ed8 100644 --- a/src/Idris/REPL/Common.idr +++ b/src/Idris/REPL/Common.idr @@ -227,6 +227,7 @@ data REPLResult : Type where ErrorsBuildingFile : String -> List Error -> REPLResult NoFileLoaded : REPLResult CurrentDirectory : String -> REPLResult + CompilationFailed: REPLResult Compiled : String -> REPLResult ProofFound : IPTerm -> REPLResult Missed : List MissedResult -> REPLResult