@@ -167,7 +167,7 @@ startServer port orig fn_in = do tid <- runIO $ forkIO (serverLoop port)
168 loop fn ist sock
168 loop fn ist sock
169 = do (s, _) <- accept sock
169 = do (s, _) <- accept sock
170− h <- socketToHandle s ReadWriteMode
170+ h <- socketToHandle s ReadWriteMode
171 hSetEncoding h utf8
171 hSetEncoding h utf8
172 cmd <- hGetLine h
172 cmd <- hGetLine h
173 let isth = case idris_outputmode ist of
173 let isth = case idris_outputmode ist of
@@ -1233,8 +1233,8 @@ process fn (Prove mode n')
1233 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
1233 let metavars = mapMaybe (\n -> do c <- lookup n (idris_metavars ist); return (n, c)) ns
1234 n <- case metavars of
1234 n <- case metavars of
1235 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
1235 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
1236− [(n, (_,_,_,False,_))] -> return n
1236+ [(n, (_,_,_,False,_))] -> return n
1237− [(_, (_,_,_,_,False))] -> ierror (Msg "Can't prove this hole as it depends on other holes")
1237+ [(_, (_,_,_,_,False))] -> ierror (Msg "Can't prove this hole as it depends on other holes")
1238 [(_, (_,_,_,True,_))] -> ierror (Msg "Declarations not solvable using prover")
1238 [(_, (_,_,_,True,_))] -> ierror (Msg "Declarations not solvable using prover")
1239 ns -> ierror (CantResolveAlts (map fst ns))
1239 ns -> ierror (CantResolveAlts (map fst ns))
1240 prover (toplevelWith fn) mode (lit fn) n
1240 prover (toplevelWith fn) mode (lit fn) n