mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-13 10:58:23 +03:00
Distinguish success and failure when returning to the OS. Fixes #390
Currently we only distinguish between success and failure, but in the future we could add more error codes if that would be useful. XXX: Mostly the code is written to return an `CommandExitCode` and then exit at the top level, but there are a few functions that exit directly (e.g., the setup function). It would be nice to clean that up.
This commit is contained in:
parent
08a7982a46
commit
09dc9b4655
@ -13,7 +13,7 @@ module Main where
|
||||
|
||||
import OptParser
|
||||
|
||||
import Cryptol.REPL.Command (loadCmd,loadPrelude)
|
||||
import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandExitCode(..))
|
||||
import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
|
||||
io,prependSearchPath,setSearchPath)
|
||||
import qualified Cryptol.REPL.Monad as REPL
|
||||
@ -33,7 +33,7 @@ import System.Console.GetOpt
|
||||
(OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
|
||||
import System.Directory (getTemporaryDirectory, removeFile)
|
||||
import System.Environment (getArgs, getProgName, lookupEnv)
|
||||
import System.Exit (exitFailure)
|
||||
import System.Exit (exitFailure,exitSuccess)
|
||||
import System.FilePath (searchPathSeparator, splitSearchPath, takeDirectory)
|
||||
import System.IO (hClose, hPutStr, openTempFile)
|
||||
|
||||
@ -197,13 +197,17 @@ main = do
|
||||
| optVersion opts -> displayVersion
|
||||
| otherwise -> do
|
||||
(opts', mCleanup) <- setupCmdScript opts
|
||||
repl (optCryptolrc opts')
|
||||
(optBatch opts')
|
||||
(setupREPL opts')
|
||||
status <- repl (optCryptolrc opts')
|
||||
(optBatch opts')
|
||||
(setupREPL opts')
|
||||
case mCleanup of
|
||||
Nothing -> return ()
|
||||
Just cmdFile -> removeFile cmdFile
|
||||
|
||||
case status of
|
||||
CommandError -> exitFailure
|
||||
CommandOk -> exitSuccess
|
||||
|
||||
setupCmdScript :: Options -> IO (Options, Maybe FilePath)
|
||||
setupCmdScript opts =
|
||||
case optCommands opts of
|
||||
|
@ -18,10 +18,11 @@ import Cryptol.REPL.Trie
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (guard, join, when)
|
||||
import Control.Monad (guard, join)
|
||||
import qualified Control.Monad.Trans.Class as MTL
|
||||
import Control.Monad.Trans.Control
|
||||
import Data.Char (isAlphaNum, isSpace)
|
||||
import Data.Maybe(isJust)
|
||||
import Data.Function (on)
|
||||
import Data.List (isPrefixOf,nub,sortBy,sort)
|
||||
import System.IO (stdout)
|
||||
@ -35,70 +36,87 @@ import System.FilePath ((</>))
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
-- | Haskeline-specific repl implementation.
|
||||
repl :: Cryptolrc -> Maybe FilePath -> REPL () -> IO ()
|
||||
repl cryrc mbBatch begin =
|
||||
do settings <- setHistoryFile (replSettings isBatch)
|
||||
runREPL isBatch (runInputTBehavior behavior settings body)
|
||||
where
|
||||
body = withInterrupt $ do
|
||||
MTL.lift evalCryptolrc
|
||||
MTL.lift begin
|
||||
loop
|
||||
|
||||
-- | One REPL invocation, either form a file or from the terminal.
|
||||
crySession :: Maybe FilePath -> REPL CommandExitCode
|
||||
crySession mbBatch =
|
||||
do settings <- io (setHistoryFile (replSettings isBatch))
|
||||
let act = runInputTBehavior behavior settings (withInterrupt loop)
|
||||
if isBatch then asBatch act else act
|
||||
where
|
||||
(isBatch,behavior) = case mbBatch of
|
||||
Nothing -> (False,defaultBehavior)
|
||||
Just path -> (True,useFile path)
|
||||
|
||||
loop = do
|
||||
prompt <- MTL.lift getPrompt
|
||||
mb <- handleInterrupt (return (Just "")) (getInputLines prompt [])
|
||||
case mb of
|
||||
loop :: InputT REPL CommandExitCode
|
||||
loop =
|
||||
do ln <- getInputLines =<< MTL.lift getPrompt
|
||||
case ln of
|
||||
NoMoreLines -> return CommandOk
|
||||
Interrupted
|
||||
| isBatch -> return CommandError
|
||||
| otherwise -> loop
|
||||
NextLine line
|
||||
| all isSpace line -> loop
|
||||
| otherwise -> doCommand line
|
||||
|
||||
Just line
|
||||
| Just cmd <- parseCommand findCommandExact line -> do
|
||||
continue <- MTL.lift $ do
|
||||
handleInterrupt handleCtrlC (runCommand cmd)
|
||||
shouldContinue
|
||||
when continue loop
|
||||
doCommand txt =
|
||||
case parseCommand findCommandExact txt of
|
||||
Nothing | isBatch -> return CommandError
|
||||
| otherwise -> loop -- say somtething?
|
||||
Just cmd -> join $ MTL.lift $
|
||||
do status <- handleInterrupt (handleCtrlC CommandError) (runCommand cmd)
|
||||
case status of
|
||||
CommandError | isBatch -> return (return status)
|
||||
_ -> do goOn <- shouldContinue
|
||||
return (if goOn then loop else return status)
|
||||
|
||||
| otherwise -> loop
|
||||
|
||||
Nothing -> return ()
|
||||
data NextLine = NextLine String | NoMoreLines | Interrupted
|
||||
|
||||
getInputLines prompt ls =
|
||||
getInputLines :: String -> InputT REPL NextLine
|
||||
getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop []
|
||||
where
|
||||
loop ls prompt =
|
||||
do mb <- getInputLine prompt
|
||||
let newPropmpt = map (\_ -> ' ') prompt
|
||||
case mb of
|
||||
Nothing -> return Nothing
|
||||
Just l | not (null l) && last l == '\\' ->
|
||||
getInputLines newPropmpt (init l : ls)
|
||||
| otherwise -> return $ Just $ unlines $ reverse $ l : ls
|
||||
Nothing -> return NoMoreLines
|
||||
Just l
|
||||
| not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt
|
||||
| otherwise -> return $ NextLine $ unlines $ reverse $ l : ls
|
||||
|
||||
evalCryptolrc =
|
||||
case cryrc of
|
||||
CryrcDefault -> do
|
||||
here <- io $ getCurrentDirectory
|
||||
home <- io $ getHomeDirectory
|
||||
let dcHere = here </> ".cryptolrc"
|
||||
dcHome = home </> ".cryptolrc"
|
||||
isHere <- io $ doesFileExist dcHere
|
||||
isHome <- io $ doesFileExist dcHome
|
||||
if | isHere -> slurp dcHere
|
||||
| isHome -> slurp dcHome
|
||||
| otherwise -> whenDebug $ io $ putStrLn "no .cryptolrc found"
|
||||
CryrcFiles paths -> mapM_ slurp paths
|
||||
CryrcDisabled -> return ()
|
||||
loadCryRC :: Cryptolrc -> REPL CommandExitCode
|
||||
loadCryRC cryrc =
|
||||
case cryrc of
|
||||
CryrcDisabled -> return CommandOk
|
||||
CryrcDefault -> check [ getCurrentDirectory, getHomeDirectory ]
|
||||
CryrcFiles opts -> loadMany opts
|
||||
where
|
||||
check [] = return CommandOk
|
||||
check (place : others) =
|
||||
do dir <- io place
|
||||
let file = dir </> ".cryptolrc"
|
||||
present <- io (doesFileExist file)
|
||||
if present
|
||||
then crySession (Just file)
|
||||
else check others
|
||||
|
||||
loadMany [] = return CommandOk
|
||||
loadMany (f : fs) = do status <- crySession (Just f)
|
||||
case status of
|
||||
CommandOk -> loadMany fs
|
||||
_ -> return status
|
||||
|
||||
-- | Haskeline-specific repl implementation.
|
||||
repl :: Cryptolrc -> Maybe FilePath -> REPL () -> IO CommandExitCode
|
||||
repl cryrc mbBatch begin =
|
||||
runREPL (isJust mbBatch) $
|
||||
do status <- loadCryRC cryrc
|
||||
case status of
|
||||
CommandOk -> begin >> crySession mbBatch
|
||||
_ -> return status
|
||||
|
||||
-- | Actually read the contents of a file, but don't save the
|
||||
-- history
|
||||
--
|
||||
-- XXX: friendlier error message would be nice if the file can't be
|
||||
-- found, but since these will be specified on the command line it
|
||||
-- should be obvious what's going wrong
|
||||
slurp path = do
|
||||
let settings' = defaultSettings { autoAddHistory = False }
|
||||
runInputTBehavior (useFile path) settings' (withInterrupt loop)
|
||||
|
||||
|
||||
-- | Try to set the history file.
|
||||
|
@ -12,7 +12,7 @@
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
module Cryptol.REPL.Command (
|
||||
-- * Commands
|
||||
Command(..), CommandDescr(..), CommandBody(..)
|
||||
Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)
|
||||
, parseCommand
|
||||
, runCommand
|
||||
, splitCommand
|
||||
@ -138,6 +138,10 @@ data CommandBody
|
||||
| NoArg (REPL ())
|
||||
|
||||
|
||||
data CommandExitCode = CommandOk
|
||||
| CommandError -- XXX: More?
|
||||
|
||||
|
||||
-- | REPL command parsing.
|
||||
commands :: CommandMap
|
||||
commands = foldl insert emptyTrie commandList
|
||||
@ -210,18 +214,20 @@ genHelp cs = map cmdHelp cs
|
||||
-- Command Evaluation ----------------------------------------------------------
|
||||
|
||||
-- | Run a command.
|
||||
runCommand :: Command -> REPL ()
|
||||
runCommand :: Command -> REPL CommandExitCode
|
||||
runCommand c = case c of
|
||||
|
||||
Command cmd -> cmd `Cryptol.REPL.Monad.catch` handler
|
||||
Command cmd -> (cmd >> return CommandOk) `Cryptol.REPL.Monad.catch` handler
|
||||
where
|
||||
handler re = rPutStrLn "" >> rPrint (pp re)
|
||||
handler re = rPutStrLn "" >> rPrint (pp re) >> return CommandError
|
||||
|
||||
Unknown cmd -> rPutStrLn ("Unknown command: " ++ cmd)
|
||||
Unknown cmd -> do rPutStrLn ("Unknown command: " ++ cmd)
|
||||
return CommandError
|
||||
|
||||
Ambiguous cmd cmds -> do
|
||||
rPutStrLn (cmd ++ " is ambiguous, it could mean one of:")
|
||||
rPutStrLn ("\t" ++ intercalate ", " cmds)
|
||||
return CommandError
|
||||
|
||||
|
||||
-- Get the setting we should use for displaying values.
|
||||
@ -791,8 +797,9 @@ cdCmd f | null f = rPutStrLn $ "[error] :cd requires a path argument"
|
||||
-- C-c Handlings ---------------------------------------------------------------
|
||||
|
||||
-- XXX this should probably do something a bit more specific.
|
||||
handleCtrlC :: REPL ()
|
||||
handleCtrlC = rPutStrLn "Ctrl-C"
|
||||
handleCtrlC :: a -> REPL a
|
||||
handleCtrlC a = do rPutStrLn "Ctrl-C"
|
||||
return a
|
||||
|
||||
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
@ -304,12 +304,13 @@ unlessBatch body = do
|
||||
|
||||
-- | Run a computation in batch mode, restoring the previous isBatch
|
||||
-- flag afterwards
|
||||
asBatch :: REPL () -> REPL ()
|
||||
asBatch :: REPL a -> REPL a
|
||||
asBatch body = do
|
||||
wasBatch <- eIsBatch `fmap` getRW
|
||||
modifyRW_ $ (\ rw -> rw { eIsBatch = True })
|
||||
body
|
||||
a <- body
|
||||
modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch })
|
||||
return a
|
||||
|
||||
disableLet :: REPL ()
|
||||
disableLet = modifyRW_ (\ rw -> rw { eLetEnabled = False })
|
||||
|
Loading…
Reference in New Issue
Block a user