292ddee · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #620 from david-christiansen/issue/607

Remove uses of error from ideslave and fix colouring

commit292ddee307ba6b8afca8f094de7f3c61873c075b authorEdwin Brady <edwin.brady@gmail.com> dateMon 18 Nov 2013, 09:10 (13 years ago) parent13b182f 8b91e60

5 files changed+16−12

compare with master

unifiedsplit

src/Core/ProofState.hs+1−1 src/Idris/AbsSyntax.hs+1−1 src/Idris/IdeSlave.hs+8−8 src/Idris/Prover.hs+3−1 src/Idris/REPL.hs+3−1

src/Core/ProofState.hs+1−1

@@ -238,7 +238,7 @@ goalAtFocus :: ProofState -> TC (Binder Type)

238238goalAtFocus ps

239239 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

240240 return (goalType g)

241− | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)

241+ | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (pterm ps)

242242

243243goal :: Hole -> Term -> TC Goal

244244goal h tm = g [] tm where

src/Idris/AbsSyntax.hs+1−1

@@ -451,7 +451,7 @@ outputTy = do i <- getIState

451451

452452setIdeSlave :: Bool -> Idris ()

453453setIdeSlave True = do i <- getIState

454− putIState $ i { idris_outputmode = (IdeSlave 0) }

454+ putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }

455455setIdeSlave False = return ()

456456

457457setTargetTriple :: String -> Idris ()

src/Idris/IdeSlave.hs+8−8

@@ -103,22 +103,22 @@ sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Ju

103103sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

104104sexpToCommand _ = Nothing

105105

106−parseMessage :: String -> (SExp, Integer)

106+parseMessage :: String -> Either Err (SExp, Integer)

107107parseMessage x = case receiveString x of

108− (SexpList [cmd, (IntegerAtom id)]) ->

109− (cmd, id)

108+ Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)

109+ Left err -> Left err

110110

111−receiveString :: String -> SExp

111+receiveString :: String -> Either Err SExp

112112receiveString x =

113113 case readHex (take 6 x) of

114114 ((num, ""):_) ->

115115 let msg = drop 6 x in

116116 if (length msg) /= (num - 1)

117− then error "bad input length"

117+ then Left . Msg $ "bad input length"

118118 else (case parseSExp msg of

119− Left _ -> error "parse failure"

120− Right r -> r)

121− _ -> error "readHex failed"

119+ Left _ -> Left . Msg $ "parse failure"

120+ Right r -> Right r)

121+ _ -> Left . Msg $ "readHex failed"

122122

123123convSExp :: SExpable a => String -> a -> Integer -> String

124124convSExp pre s id =

src/Idris/Prover.hs+3−1

@@ -137,7 +137,9 @@ receiveInput :: ElabState [PDecl] -> Idris (Maybe String)

137137receiveInput e =

138138 do i <- getIState

139139 l <- runIO $ getLine

140− let (sexp, id) = parseMessage l

140+ (sexp, id) <- case parseMessage l of

141+ Left err -> ierror err

142+ Right (sexp, id) -> return (sexp, id)

141143 putIState $ i { idris_outputmode = (IdeSlave id) }

142144 case sexpToCommand sexp of

143145 Just (REPLCompletions prefix) ->

src/Idris/REPL.hs+3−1

@@ -192,7 +192,9 @@ ideslave :: IState -> [FilePath] -> Idris ()

192192ideslave orig mods

193193 = do idrisCatch

194194 (do l <- runIO $ getLine

195− let (sexp, id) = parseMessage l

195+ (sexp, id) <- case parseMessage l of

196+ Left err -> ierror err

197+ Right (sexp, id) -> return (sexp, id)

196198 i <- getIState

197199 putIState $ i { idris_outputmode = (IdeSlave id) }

198200 case sexpToCommand sexp of