idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 09:49:24 +03:00
Code Issues Projects Releases Wiki Activity

Use double quotes to display the current working directory

Browse Source
This commit is contained in:
Kamil Shakirov 2021-02-15 18:35:45 +06:00 committed by G. Allais
parent b355b12cdb
commit 357e2a4cf6
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/IDEMode/REPL.idr
View File

@ -328,7 +328,7 @@ displayIDEResult outf i (REPL $ NoFileLoaded)
= printIDEError outf i $ reflow "No file can be reloaded"
displayIDEResult outf i (REPL $ CurrentDirectory dir)
= printIDEResult outf i
$ StringAtom $ "Current working directory is '" ++ dir ++ "'"
$ StringAtom $ "Current working directory is \"" ++ dir ++ "\""
displayIDEResult outf i (REPL CompilationFailed)
= printIDEError outf i $ reflow "Compilation failed"
displayIDEResult outf i (REPL $ Compiled f)

2
src/Idris/REPL.idr
View File

@ -1044,7 +1044,7 @@ mutual
displayResult (ErrorLoadingFile x err) = printResult (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err))
displayResult (ErrorsBuildingFile x errs) = printResult (reflow "Error(s) building file" <++> pretty x) -- messages already displayed while building
displayResult NoFileLoaded = printError (reflow "No file can be reloaded")
displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> squotes (pretty dir))
displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> dquotes (pretty dir))
displayResult CompilationFailed = printError (reflow "Compilation failed")
displayResult (Compiled f) = printResult (pretty "File" <++> pretty f <++> pretty "written")
displayResult (ProofFound x) = printResult (prettyTerm x)