git.iko.soy/Idris-dev
on master help sign in
IdeSlave mode improvements:
674c8b8Hannes Mehnert
src/Idris/AbsSyntax.hs+31−2
compare with master
unifiedsplit
@@ -241,14 +241,43 @@ solveDeferred :: Name -> Idris ()
241solveDeferred n = do i <- getIState
241solveDeferred n = do i <- getIState
242 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
242 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
243
243
244+iResult :: String -> Idris ()
245+iResult s = do i <- getIState
246+ case idris_outputmode i of
247+ RawOutput -> case s of
248+ "" -> return ()
249+ s -> liftIO $ putStrLn s
250+ IdeSlave n ->
251+ let good = List [SymbolAtom "ok", toSExp s] in
252+ liftIO $ putStrLn $ convSExp "return" good n
253+
254+iFail :: String -> Idris ()
255+iFail s = do i <- getIState
256+ case idris_outputmode i of
257+ RawOutput -> case s of
258+ "" -> return ()
259+ s -> liftIO $ putStrLn s
260+ IdeSlave n ->
261+ let good = List [SymbolAtom "error", toSExp s] in
262+ liftIO $ putStrLn $ convSExp "return" good n
263+
244iputStrLn :: String -> Idris ()
264iputStrLn :: String -> Idris ()
245iputStrLn s = do i <- getIState
265iputStrLn s = do i <- getIState
246 case idris_outputmode i of
266 case idris_outputmode i of
247 RawOutput -> liftIO $ putStrLn s
267 RawOutput -> liftIO $ putStrLn s
268+ IdeSlave n ->
269+ case span (/=':') s of
270+ (fn, ':':rest) -> case span isDigit rest of
271+ ([], ':':msg) -> iWarn (FC fn 0) msg
272+ ([], msg) -> iWarn (FC fn 0) msg
273+ (num, ':':msg) -> iWarn (FC fn (read num)) msg
248− IdeSlave n -> liftIO $ putStrLn $ convSExp "write-string" s n
274+ _ -> liftIO $ putStrLn $ convSExp "write-string" s n
249
275
250iWarn :: FC -> String -> Idris ()
276iWarn :: FC -> String -> Idris ()
277+iWarn fc err = do i <- getIState
278+ case idris_outputmode i of
251−iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
279+ RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)
280+ IdeSlave n -> liftIO $ putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
252
281
253setLogLevel :: Int -> Idris ()
282setLogLevel :: Int -> Idris ()
254setLogLevel l = do i <- getIState
283setLogLevel l = do i <- getIState
src/Idris/IdeSlave.hs+8−12
@@ -1,6 +1,6 @@
1{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}
1{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}
2
2
3−module Idris.IdeSlave(receiveMessage, sendMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, SExp(..)) where
3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..)) where
4
4
5import Text.Printf
5import Text.Printf
6import Numeric
6import Numeric
@@ -55,6 +55,9 @@ instance (SExpable a) => SExpable [a] where
55instance (SExpable a, SExpable b) => SExpable (a, b) where
55instance (SExpable a, SExpable b) => SExpable (a, b) where
56 toSExp (l, r) = List [toSExp l, toSExp r]
56 toSExp (l, r) = List [toSExp l, toSExp r]
57
57
58+instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
59+ toSExp (l, m, n) = List [toSExp l, toSExp m, toSExp n]
60+
58escape :: String -> String
61escape :: String -> String
59escape = concatMap escapeChar
62escape = concatMap escapeChar
60 where
63 where
@@ -96,10 +99,10 @@ sexpToCommand (List [SymbolAtom "repl-completions", StringAtom prefix]) = Just (
96sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)
99sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)
97sexpToCommand _ = Nothing
100sexpToCommand _ = Nothing
98
101
99−receiveMessage :: String -> (SExp, Integer)
102+parseMessage :: String -> (SExp, Integer)
100−receiveMessage x = case receiveString x of
103+parseMessage x = case receiveString x of
101− (List [cmd, (IntegerAtom id)]) ->
104+ (List [cmd, (IntegerAtom id)]) ->
102− (cmd, id)
105+ (cmd, id)
103
106
104receiveString :: String -> SExp
107receiveString :: String -> SExp
105receiveString x =
108receiveString x =
@@ -119,12 +122,5 @@ convSExp pre s id =
119 let str = sExpToString sex in
122 let str = sExpToString sex in
120 (getHexLength str) ++ str
123 (getHexLength str) ++ str
121
124
122−sendMessage :: SExpable a => Integer -> Either a a -> String
123−sendMessage id s =
124− let sexp = case s of
125− Left err -> List [SymbolAtom "error", toSExp err]
126− Right succ -> List [SymbolAtom "ok", toSExp succ]
127− in convSExp "return" sexp id
128−
129getHexLength :: String -> String
125getHexLength :: String -> String
130getHexLength s = printf "%06x" (1 + (length s))
126getHexLength s = printf "%06x" (1 + (length s))
src/Idris/REPL.hs+134−74
@@ -82,45 +82,102 @@ repl orig mods
82 repl orig mods
82 repl orig mods
83
83
84-- | Run the IdeSlave
84-- | Run the IdeSlave
85−ideslaveStart :: [FilePath] -> Idris ()
85+ideslaveStart :: IState -> [FilePath] -> Idris ()
86−ideslaveStart mods
86+ideslaveStart orig mods
87 = do i <- getIState
87 = do i <- getIState
88 case idris_outputmode i of
88 case idris_outputmode i of
89 IdeSlave n ->
89 IdeSlave n ->
90 when (mods /= []) (do liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt mods) n)
90 when (mods /= []) (do liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt mods) n)
91− ideslave mods
91+ ideslave orig mods
92
92
93
93
94−ideslave :: [FilePath] -> Idris ()
94+ideslave :: IState -> [FilePath] -> Idris ()
95−ideslave mods
95+ideslave orig mods
96 = do idrisCatch
96 = do idrisCatch
97 (do l <- liftIO $ getLine
97 (do l <- liftIO $ getLine
98− let (sexp, id) = receiveMessage l
98+ let (sexp, id) = parseMessage l
99 i <- getIState
99 i <- getIState
100 putIState $ i { idris_outputmode = (IdeSlave id) }
100 putIState $ i { idris_outputmode = (IdeSlave id) }
101 case sexpToCommand sexp of
101 case sexpToCommand sexp of
102 Just (Interpret cmd) ->
102 Just (Interpret cmd) ->
103− do i <- getIState
104− let fn = case mods of
103+ do let fn = case mods of
105− (f:_) -> f
104+ (f:_) -> f
106− _ -> ""
105+ _ -> ""
107 case parseCmd i cmd of
106 case parseCmd i cmd of
108− Left err -> do liftIO $ putStrLn $ sendMessage id (Left (show err))
107+ Left err -> iFail $ show err
109− Right cmd -> do idrisCatch
108+ Right cmd -> idrisCatch
110− (do xs <- process fn cmd
109+ (do ideslaveProcess fn cmd)
111− liftIO $ putStrLn $ sendMessage id (Right (xs, "no output")))
110+ (\e -> do iFail $ show e)
112− (\e -> do liftIO $ putStrLn $ sendMessage id (Left (show e)))
113 Just (REPLCompletions str) ->
111 Just (REPLCompletions str) ->
114 do (unused, compls) <- replCompletion (reverse str, "")
112 do (unused, compls) <- replCompletion (reverse str, "")
115− liftIO $ putStrLn $ sendMessage id (Right (map replacement compls, reverse unused))
113+ let good = List [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
114+ liftIO $ putStrLn $ convSExp "return" good id
116− Just (LoadFile filename) -> do clearErr
115+ Just (LoadFile filename) ->
116+ do clearErr
117+ putIState (orig { idris_options = idris_options i,
118+ idris_outputmode = (IdeSlave id) })
117− mod <- loadModule filename
119+ loadModule filename
120+ iucheck
118− liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id
121+ liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id
119− liftIO $ putStrLn $ sendMessage id (Right (SymbolAtom "good"))
122+ -- report success! or failure!
120− ideslave [filename]
123+ ideslave orig [filename]
121− Nothing -> do liftIO $ putStrLn $ sendMessage id (Left "did not understand"))
124+ Nothing -> do iFail "did not understand")
122− (\e -> do liftIO $ putStrLn $ sendMessage 0 (Left (show e)))
125+ (\e -> do iFail $ show e)
123− ideslave mods
126+ ideslave orig mods
127+
128+ideslaveProcess :: FilePath -> Command -> Idris ()
129+ideslaveProcess fn Help = process fn Help
130+ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)
131+ iResult "changed directory to"
132+ideslaveProcess fn (Eval t) = process fn (Eval t)
133+ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)
134+ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
135+ideslaveProcess fn (Check t) = process fn (Check t)
136+ideslaveProcess fn (DocStr n) = process fn (DocStr n)
137+ideslaveProcess fn Universes = process fn Universes
138+ideslaveProcess fn (Defn n) = do process fn (Defn n)
139+ iResult ""
140+ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)
141+ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)
142+ iResult ""
143+ideslaveProcess fn (Info n) = process fn (Info n)
144+ideslaveProcess fn (Search t) = process fn (Search t)
145+ideslaveProcess fn (Spec t) = process fn (Spec t)
146+-- RmProof and AddProof not supported!
147+ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
148+ideslaveProcess fn (Prove n') = process fn (Prove n')
149+ideslaveProcess fn (HNF t) = process fn (HNF t)
150+--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
151+
152+--that most likely does not work, since we need to wrap
153+--input/output of the executed binary...
154+ideslaveProcess fn Execute = do process fn Execute
155+ iResult ""
156+ideslaveProcess fn (NewCompile f) = do process fn (NewCompile f)
157+ iResult ""
158+ideslaveProcess fn (Compile target f) = do process fn (Compile target f)
159+ iResult ""
160+ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)
161+ iResult ""
162+ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)
163+ideslaveProcess fn (Missing n) = process fn (Missing n)
164+ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)
165+ iResult ""
166+ideslaveProcess fn ListDynamic = do process fn ListDynamic
167+ iResult ""
168+ideslaveProcess fn Metavars = process fn Metavars
169+ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
170+ iResult ""
171+ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
172+ iResult ""
173+ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
174+ iResult ""
175+ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
176+ iResult ""
177+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)
178+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
179+ideslaveProcess fn _ = iFail "command not recognized or not supported"
180+
124
181
125-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
182-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
126mkPrompt [] = "Idris"
183mkPrompt [] = "Idris"
@@ -215,25 +272,25 @@ proofs orig
215
272
216insertScript :: String -> [String] -> [String]
273insertScript :: String -> [String] -> [String]
217insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
274insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
218−insertScript prf (p@"---------- Proofs ----------" : "" : xs)
275+insertScript prf (p@"---------- Proofs ----------" : "" : xs)
219 = p : "" : prf : xs
276 = p : "" : prf : xs
220insertScript prf (x : xs) = x : insertScript prf xs
277insertScript prf (x : xs) = x : insertScript prf xs
221
278
222process :: FilePath -> Command -> Idris ()
279process :: FilePath -> Command -> Idris ()
223−process fn Help = iputStrLn displayHelp
280+process fn Help = iResult displayHelp
224process fn (ChangeDirectory f)
281process fn (ChangeDirectory f)
225 = do liftIO $ setCurrentDirectory f
282 = do liftIO $ setCurrentDirectory f
226 return ()
283 return ()
227−process fn (Eval t)
284+process fn (Eval t)
228 = do (tm, ty) <- elabVal toplevel False t
285 = do (tm, ty) <- elabVal toplevel False t
229 ctxt <- getContext
286 ctxt <- getContext
230− ist <- getIState
287+ ist <- getIState
231 let tm' = normaliseAll ctxt [] tm
288 let tm' = normaliseAll ctxt [] tm
232 let ty' = normaliseAll ctxt [] ty
289 let ty' = normaliseAll ctxt [] ty
233 logLvl 3 $ "Raw: " ++ show (tm', ty')
290 logLvl 3 $ "Raw: " ++ show (tm', ty')
234 imp <- impShow
291 imp <- impShow
235− iputStrLn (showImp imp (delab ist tm') ++ " : " ++
292+ iResult (showImp imp (delab ist tm') ++ " : " ++
236− showImp imp (delab ist ty'))
293+ showImp imp (delab ist ty'))
237process fn (ExecVal t)
294process fn (ExecVal t)
238 = do ctxt <- getContext
295 = do ctxt <- getContext
239 ist <- getIState
296 ist <- getIState
@@ -242,30 +299,31 @@ process fn (ExecVal t)
242 let ty' = normaliseAll ctxt [] ty
299 let ty' = normaliseAll ctxt [] ty
243 res <- execute tm
300 res <- execute tm
244 imp <- impShow
301 imp <- impShow
245− iputStrLn (showImp imp (delab ist res) ++ " : " ++
302+ iResult (showImp imp (delab ist res) ++ " : " ++
246− showImp imp (delab ist ty'))
303+ showImp imp (delab ist ty'))
247− return ()
248process fn (Check (PRef _ n))
304process fn (Check (PRef _ n))
249 = do ctxt <- getContext
305 = do ctxt <- getContext
250 ist <- getIState
306 ist <- getIState
251 imp <- impShow
307 imp <- impShow
252 case lookupNames n ctxt of
308 case lookupNames n ctxt of
253− ts@(_:_) -> mapM_ (\n -> iputStrLn $ show n ++ " : " ++
309+ ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++
254− showImp imp (delabTy ist n)) ts
310+ showImp imp (delabTy ist n)) ts
311+ iResult ""
255− [] -> iputStrLn $ "No such variable " ++ show n
312+ [] -> iFail $ "No such variable " ++ show n
256process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
313process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
257 ctxt <- getContext
314 ctxt <- getContext
258− ist <- getIState
315+ ist <- getIState
259 imp <- impShow
316 imp <- impShow
260 let ty' = normaliseC ctxt [] ty
317 let ty' = normaliseC ctxt [] ty
261− iputStrLn (showImp imp (delab ist tm) ++ " : " ++
318+ iResult (showImp imp (delab ist tm) ++ " : " ++
262− showImp imp (delab ist ty))
319+ showImp imp (delab ist ty))
263
320
264process fn (DocStr n) = do i <- getIState
321process fn (DocStr n) = do i <- getIState
265 case lookupCtxtName n (idris_docstrings i) of
322 case lookupCtxtName n (idris_docstrings i) of
266− [] -> iputStrLn $ "No documentation for " ++ show n
323+ [] -> iFail $ "No documentation for " ++ show n
267− ns -> mapM_ showDoc ns
324+ ns -> do mapM_ showDoc ns
325+ iResult ""
268− where showDoc (n, d)
326+ where showDoc (n, d)
269 = do doc <- getDocs n
327 = do doc <- getDocs n
270 iputStrLn $ show doc
328 iputStrLn $ show doc
271process fn Universes = do i <- getIState
329process fn Universes = do i <- getIState
@@ -275,8 +333,8 @@ process fn Universes = do i <- getIState
275 let n = length cs
333 let n = length cs
276 iputStrLn $ "(" ++ show n ++ " constraints)"
334 iputStrLn $ "(" ++ show n ++ " constraints)"
277 case ucheck cs of
335 case ucheck cs of
278− Error e -> iputStrLn $ pshow i e
336+ Error e -> iFail $ pshow i e
279− OK _ -> iputStrLn "Universes OK"
337+ OK _ -> iResult "Universes OK"
280process fn (Defn n) = do i <- getIState
338process fn (Defn n) = do i <- getIState
281 iputStrLn "Compiled patterns:\n"
339 iputStrLn "Compiled patterns:\n"
282 liftIO $ print (lookupDef n (tt_ctxt i))
340 liftIO $ print (lookupDef n (tt_ctxt i))
@@ -287,14 +345,15 @@ process fn (Defn n) = do i <- getIState
287 case lookupTotal n (tt_ctxt i) of
345 case lookupTotal n (tt_ctxt i) of
288 [t] -> iputStrLn (showTotal t i)
346 [t] -> iputStrLn (showTotal t i)
289 _ -> return ()
347 _ -> return ()
290− where printCase i (_, lhs, rhs)
348+ where printCase i (_, lhs, rhs)
291 = do iputStrLn (showImp True (delab i lhs) ++ " = " ++
349 = do iputStrLn (showImp True (delab i lhs) ++ " = " ++
292 showImp True (delab i rhs))
350 showImp True (delab i rhs))
293process fn (TotCheck n) = do i <- getIState
351process fn (TotCheck n) = do i <- getIState
294 case lookupTotal n (tt_ctxt i) of
352 case lookupTotal n (tt_ctxt i) of
295− [t] -> iputStrLn (showTotal t i)
353+ [t] -> iResult (showTotal t i)
354+ _ -> do iFail ""
296− _ -> return ()
355+ return ()
297−process fn (DebugInfo n)
356+process fn (DebugInfo n)
298 = do i <- getIState
357 = do i <- getIState
299 let oi = lookupCtxtName n (idris_optimisation i)
358 let oi = lookupCtxtName n (idris_optimisation i)
300 when (not (null oi)) $ iputStrLn (show oi)
359 when (not (null oi)) $ iputStrLn (show oi)
@@ -316,13 +375,13 @@ process fn (DebugInfo n)
316process fn (Info n) = do i <- getIState
375process fn (Info n) = do i <- getIState
317 case lookupCtxt n (idris_classes i) of
376 case lookupCtxt n (idris_classes i) of
318 [c] -> classInfo c
377 [c] -> classInfo c
319− _ -> iputStrLn "Not a class"
378+ _ -> iFail "Not a class"
320−process fn (Search t) = iputStrLn "Not implemented"
379+process fn (Search t) = iFail "Not implemented"
321process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
380process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
322 ctxt <- getContext
381 ctxt <- getContext
323 ist <- getIState
382 ist <- getIState
324 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
383 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
325− iputStrLn (show (delab ist tm'))
384+ iResult (show (delab ist tm'))
326
385
327process fn (RmProof n')
386process fn (RmProof n')
328 = do i <- getIState
387 = do i <- getIState
@@ -374,8 +433,8 @@ process fn (ShowProof n')
374 n <- resolveProof n'
433 n <- resolveProof n'
375 let proofs = proof_list i
434 let proofs = proof_list i
376 case lookup n proofs of
435 case lookup n proofs of
377− Nothing -> iputStrLn "No proof to show"
436+ Nothing -> iFail "No proof to show"
378− Just p -> iputStrLn $ showProof False n p
437+ Just p -> iResult $ showProof False n p
379
438
380process fn (Prove n')
439process fn (Prove n')
381 = do ctxt <- getContext
440 = do ctxt <- getContext
@@ -395,13 +454,13 @@ process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
395 ctxt <- getContext
454 ctxt <- getContext
396 ist <- getIState
455 ist <- getIState
397 let tm' = hnf ctxt [] tm
456 let tm' = hnf ctxt [] tm
398− iputStrLn (show (delab ist tm'))
457+ iResult (show (delab ist tm'))
399process fn TTShell = do ist <- getIState
458process fn TTShell = do ist <- getIState
400 let shst = initState (tt_ctxt ist)
459 let shst = initState (tt_ctxt ist)
401 runShell shst
460 runShell shst
402 return ()
461 return ()
403−process fn Execute = do (m, _) <- elabVal toplevel False
462+process fn Execute = do (m, _) <- elabVal toplevel False
404− (PApp fc
463+ (PApp fc
405 (PRef fc (UN "run__IO"))
464 (PRef fc (UN "run__IO"))
406 [pexp $ PRef fc (NS (UN "main") ["Main"])])
465 [pexp $ PRef fc (NS (UN "main") ["Main"])])
407-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
466-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
@@ -411,37 +470,37 @@ process fn Execute = do (m, _) <- elabVal toplevel False
411 compile t tmpn m
470 compile t tmpn m
412 liftIO $ system tmpn
471 liftIO $ system tmpn
413 return ()
472 return ()
414− where fc = FC "main" 0
473+ where fc = FC "main" 0
415−process fn (NewCompile f)
474+process fn (NewCompile f)
416 = do (m, _) <- elabVal toplevel False
475 = do (m, _) <- elabVal toplevel False
417 (PApp fc (PRef fc (UN "run__IO"))
476 (PApp fc (PRef fc (UN "run__IO"))
418 [pexp $ PRef fc (NS (UN "main") ["Main"])])
477 [pexp $ PRef fc (NS (UN "main") ["Main"])])
419 compileEpic f m
478 compileEpic f m
420− where fc = FC "main" 0
479+ where fc = FC "main" 0
421−process fn (Compile target f)
480+process fn (Compile target f)
422 = do (m, _) <- elabVal toplevel False
481 = do (m, _) <- elabVal toplevel False
423 (PApp fc (PRef fc (UN "run__IO"))
482 (PApp fc (PRef fc (UN "run__IO"))
424 [pexp $ PRef fc (NS (UN "main") ["Main"])])
483 [pexp $ PRef fc (NS (UN "main") ["Main"])])
425 compile target f m
484 compile target f m
426− where fc = FC "main" 0
485+ where fc = FC "main" 0
427−process fn (LogLvl i) = setLogLevel i
486+process fn (LogLvl i) = setLogLevel i
428-- Elaborate as if LHS of a pattern (debug command)
487-- Elaborate as if LHS of a pattern (debug command)
429−process fn (Pattelab t)
488+process fn (Pattelab t)
430 = do (tm, ty) <- elabVal toplevel True t
489 = do (tm, ty) <- elabVal toplevel True t
431− iputStrLn $ show tm ++ "\n\n : " ++ show ty
490+ iResult $ show tm ++ "\n\n : " ++ show ty
432
491
433−process fn (Missing n)
492+process fn (Missing n)
434 = do i <- getIState
493 = do i <- getIState
435 case lookupCtxt n (idris_patdefs i) of
494 case lookupCtxt n (idris_patdefs i) of
436 [] -> return ()
495 [] -> return ()
437− [(_, tms)] ->
496+ [(_, tms)] ->
438− iputStrLn (showSep "\n" (map (showImp True) tms))
497+ iResult (showSep "\n" (map (showImp True) tms))
439− _ -> iputStrLn $ "Ambiguous name"
498+ _ -> iFail $ "Ambiguous name"
440process fn (DynamicLink l) = do i <- getIState
499process fn (DynamicLink l) = do i <- getIState
441 let lib = trim l
500 let lib = trim l
442 handle <- lift $ tryLoadLib lib
501 handle <- lift $ tryLoadLib lib
443 case handle of
502 case handle of
444− Nothing -> iputStrLn $ "Could not load dynamic lib \"" ++ l ++ "\""
503+ Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""
445 Just x -> do let libs = idris_dynamic_libs i
504 Just x -> do let libs = idris_dynamic_libs i
446 putIState $ i { idris_dynamic_libs = x:libs }
505 putIState $ i { idris_dynamic_libs = x:libs }
447 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
506 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
@@ -454,8 +513,8 @@ process fn Metavars
454 = do ist <- getIState
513 = do ist <- getIState
455 let mvs = idris_metavars ist \\ primDefs
514 let mvs = idris_metavars ist \\ primDefs
456 case mvs of
515 case mvs of
457− [] -> iputStrLn "No global metavariables to solve"
516+ [] -> iFail "No global metavariables to solve"
458− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
517+ _ -> iResult $ "Global metavariables:\n\t" ++ show mvs
459process fn NOP = return ()
518process fn NOP = return ()
460
519
461process fn (SetOpt ErrContext) = setErrContext True
520process fn (SetOpt ErrContext) = setErrContext True
@@ -463,8 +522,8 @@ process fn (UnsetOpt ErrContext) = setErrContext False
463process fn (SetOpt ShowImpl) = setImpShow True
522process fn (SetOpt ShowImpl) = setImpShow True
464process fn (UnsetOpt ShowImpl) = setImpShow False
523process fn (UnsetOpt ShowImpl) = setImpShow False
465
524
466−process fn (SetOpt _) = iputStrLn "Not a valid option"
525+process fn (SetOpt _) = iFail "Not a valid option"
467−process fn (UnsetOpt _) = iputStrLn "Not a valid option"
526+process fn (UnsetOpt _) = iFail "Not a valid option"
468
527
469
528
470classInfo :: ClassInfo -> Idris ()
529classInfo :: ClassInfo -> Idris ()
@@ -473,6 +532,7 @@ classInfo ci = do iputStrLn "Methods:\n"
473 iputStrLn ""
532 iputStrLn ""
474 iputStrLn "Instances:\n"
533 iputStrLn "Instances:\n"
475 mapM_ dumpInstance (class_instances ci)
534 mapM_ dumpInstance (class_instances ci)
535+ iResult ""
476
536
477dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
537dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
478dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
538dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
@@ -622,7 +682,7 @@ idrisMain opts =
622 [] -> return ()
682 [] -> return ()
623 (o:_) -> process "" (NewCompile o)
683 (o:_) -> process "" (NewCompile o)
624 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
684 when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
625− when (idesl) $ ideslaveStart inputs
685+ when (idesl) $ ideslaveStart ist inputs
626 ok <- noErrors
686 ok <- noErrors
627 when (not ok) $ liftIO (exitWith (ExitFailure 1))
687 when (not ok) $ liftIO (exitWith (ExitFailure 1))
628 where
688 where