File tree 3 files changed +4
-0
lines changed
3 files changed +4
-0
lines changed Original file line number Diff line number Diff line change @@ -351,6 +351,8 @@ displayIDEResult outf i (REPL $ NoFileLoaded)
351
351
= printIDEError outf i $ reflow " No file can be reloaded"
352
352
displayIDEResult outf i (REPL $ CurrentDirectory dir)
353
353
= printIDEResult outf i $ AString $ " Current working directory is \" \{dir}\" "
354
+ displayIDEResult outf i (REPL CompilationFailed )
355
+ = printIDEError outf i $ reflow " Compilation failed"
354
356
displayIDEResult outf i (REPL $ Compiled f)
355
357
= printIDEResult outf i $ AString " File \{f} written"
356
358
displayIDEResult outf i (REPL $ ProofFound x)
Original file line number Diff line number Diff line change @@ -1260,6 +1260,7 @@ mutual
1260
1260
displayResult NoFileLoaded = printResult (reflow " No file can be reloaded" )
1261
1261
displayResult (CurrentDirectory dir)
1262
1262
= printResult (reflow " Current working directory is" <++> dquotes (pretty0 dir))
1263
+ displayResult CompilationFailed = printResult (reflow " Compilation failed" )
1263
1264
displayResult (Compiled f) = printResult (" File" <++> pretty0 f <++> " written" )
1264
1265
displayResult (ProofFound x) = printResult (prettyBy Syntax x)
1265
1266
displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases)
Original file line number Diff line number Diff line change @@ -227,6 +227,7 @@ data REPLResult : Type where
227
227
ErrorsBuildingFile : String -> List Error -> REPLResult
228
228
NoFileLoaded : REPLResult
229
229
CurrentDirectory : String -> REPLResult
230
+ CompilationFailed : REPLResult
230
231
Compiled : String -> REPLResult
231
232
ProofFound : IPTerm -> REPLResult
232
233
Missed : List MissedResult -> REPLResult
You can’t perform that action at this time.
0 commit comments