f18d79c · Idris-dev · git.iko.soy

src/Core/ProofState.hs+1−1

compare with master

unifiedsplit

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

238goalAtFocus ps

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

240 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)

242

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

244goal h tm = g [] tm where

src/Idris/IdeSlave.hs+8−8

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

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

104sexpToCommand _ = Nothing

105

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

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

107parseMessage x = case receiveString x of

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

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

109− (cmd, id)

109+ Left err -> Left err

110

111−receiveString :: String -> SExp

111+receiveString :: String -> Either Err SExp

112receiveString x =

113 case readHex (take 6 x) of

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

115 let msg = drop 6 x in

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

117− then error "bad input length"

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

118 else (case parseSExp msg of

119− Left _ -> error "parse failure"

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

120− Right r -> r)

120+ Right r -> Right r)

121− _ -> error "readHex failed"

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

122

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

124convSExp pre s id =

src/Idris/Prover.hs+3−1

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

137receiveInput e =

138 do i <- getIState

139 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)

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

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

142 case sexpToCommand sexp of

144 case sexpToCommand sexp of

143 Just (REPLCompletions prefix) ->

145 Just (REPLCompletions prefix) ->

src/Idris/REPL.hs+3−1

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

192ideslave orig mods

193 = do idrisCatch

194 (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)

196 i <- getIState

198 i <- getIState

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

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

198 case sexpToCommand sexp of

200 case sexpToCommand sexp of