edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-22 04:11:31 +03:00
Code Issues Projects Releases Wiki Activity

Add a case in the repl for empty command

Browse Source 
Changes to be committed:
	modified:   src/Idris/REPL.idr
This commit is contained in:
Andre Kuhlenschmidt 2019-08-14 16:41:58 -04:00
parent a87a3c14c2
commit 20a2cc0f31
1 changed files with 18 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/Idris/REPL.idr
View File

@ -549,8 +549,7 @@ process (Editing cmd)
setPPrint ppopts setPPrint ppopts
pure True pure True
process Quit process Quit
= do iputStrLn "Bye for now!" = pure False
pure False
processCatch : {auto c : Ref Ctxt Defs} -> processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
@ -574,11 +573,17 @@ processCatch cmd
coreLift (putStrLn !(display err)) coreLift (putStrLn !(display err))
pure True) pure True)
parseRepl : String -> Either ParseError REPLCmd parseEmptyCmd : EmptyRule (Maybe REPLCmd)
parseEmptyCmd = eoi *> (pure Nothing)
parseCmd : Rule (Maybe REPLCmd)
parseCmd = do c <- command; eoi; pure $ Just c
parseRepl : String -> Either ParseError (Maybe REPLCmd)
parseRepl inp parseRepl inp
= case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
Nothing => runParser inp (do c <- command; eoi; pure c) Nothing => runParser inp (parseEmptyCmd <|> parseCmd)
Just cmd => Right cmd Just cmd => Right $ Just cmd
where where
-- a right load of hackery - we can't tokenise the filename using the -- a right load of hackery - we can't tokenise the filename using the
-- ordinary parser. There's probably a better way... -- ordinary parser. There's probably a better way...
@ -603,7 +608,8 @@ interpret inp
= case parseRepl inp of = case parseRepl inp of
Left err => do printError (show err) Left err => do printError (show err)
pure True pure True
Right cmd => processCatch cmd Right Nothing => pure True
Right (Just cmd) => processCatch cmd
export export
repl : {auto c : Ref Ctxt Defs} -> repl : {auto c : Ref Ctxt Defs} ->
@ -617,12 +623,13 @@ repl
opts <- get ROpts opts <- get ROpts
coreLift (putStr (prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> ")) coreLift (putStr (prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> "))
inp <- coreLift getLine inp <- coreLift getLine
repeat <- interpret inp
end <- coreLift $ fEOF stdin end <- coreLift $ fEOF stdin
if end if repeat && not end
then iputStrLn "Bye for now!" then repl
else if !(interpret inp) else
then repl do coreLift $ putStrLn "Bye for now!"
else pure () pure ()
where where
prompt : REPLEval -> String prompt : REPLEval -> String