mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-07 08:18:12 +03:00
Add :! to REPL
Runs shell command
This commit is contained in:
parent
4dbfbf1943
commit
9a20564bb4
@ -800,6 +800,9 @@ process (Editing cmd)
|
||||
process (CGDirective str)
|
||||
= do setSession (record { directives $= (str::) } !getSession)
|
||||
pure Done
|
||||
process (RunShellCommand cmd)
|
||||
= do coreLift (system cmd)
|
||||
pure Done
|
||||
process Quit
|
||||
= pure Exited
|
||||
process NOP
|
||||
@ -838,7 +841,7 @@ parseCmd = do c <- command; eoi; pure $ Just c
|
||||
export
|
||||
parseRepl : String -> Either (ParseError Token) (Maybe REPLCmd)
|
||||
parseRepl inp
|
||||
= case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
|
||||
= case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD), (":!", RunShellCommand)] inp of
|
||||
Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd)
|
||||
Just cmd => Right $ Just cmd
|
||||
where
|
||||
|
@ -447,6 +447,7 @@ data REPLCmd : Type where
|
||||
SetColor : Bool -> REPLCmd
|
||||
Metavars : REPLCmd
|
||||
Editing : EditCmd -> REPLCmd
|
||||
RunShellCommand : String -> REPLCmd
|
||||
ShowVersion : REPLCmd
|
||||
Quit : REPLCmd
|
||||
NOP : REPLCmd
|
||||
|
Loading…
Reference in New Issue
Block a user