git.iko.soy/Idris-dev
on master help sign in
Merge pull request #312 from hannesm/ideslave

Ideslave option

commitf608369bb8ae09b95c596d703efc004fada50982 authorEdwin Brady <edwin.brady@gmail.com> dateSat 11 May 2013, 15:17 (13 years ago) parent99a8a66674c8b8
5 files changed+336−59
compare with master
unifiedsplit
idris.cabal+1−1 src/Idris/AbsSyntax.hs+42−2 src/Idris/AbsSyntaxTree.hs+8−2 src/Idris/IdeSlave.hs+126 src/Idris/REPL.hs+159−54
idris.cabal+1−1
@@ -90,7 +90,7 @@ Executable idris
9090 Core.CaseTree, Core.Constraints,
9191
9292 Idris.AbsSyntax, Idris.AbsSyntaxTree,
93− Idris.Parser, Idris.Help, Idris.REPL,
93+ Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL,
9494 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
9595 Idris.Delaborate, Idris.Primitives, Idris.Imports,
9696 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
src/Idris/AbsSyntax.hs+42−2
@@ -8,6 +8,7 @@ import Core.Evaluate
88import Core.Elaborate hiding (Tactic(..))
99import Core.Typecheck
1010import Idris.AbsSyntaxTree
11+import Idris.IdeSlave
1112import IRTS.CodegenCommon
1213import Util.DynamicLinker
1314
@@ -26,6 +27,8 @@ import Debug.Trace
2627import Util.Pretty
2728import Util.System
2829
30+import Text.Printf (printf)
31+
2932getContext :: Idris Context
3033getContext = do i <- getIState; return (tt_ctxt i)
3134
@@ -242,11 +245,43 @@ solveDeferred :: Name -> Idris ()
242245solveDeferred n = do i <- getIState
243246 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
244247
248+iResult :: String -> Idris ()
249+iResult s = do i <- getIState
250+ case idris_outputmode i of
251+ RawOutput -> case s of
252+ "" -> return ()
253+ s -> liftIO $ putStrLn s
254+ IdeSlave n ->
255+ let good = List [SymbolAtom "ok", toSExp s] in
256+ liftIO $ putStrLn $ convSExp "return" good n
257+
258+iFail :: String -> Idris ()
259+iFail s = do i <- getIState
260+ case idris_outputmode i of
261+ RawOutput -> case s of
262+ "" -> return ()
263+ s -> liftIO $ putStrLn s
264+ IdeSlave n ->
265+ let good = List [SymbolAtom "error", toSExp s] in
266+ liftIO $ putStrLn $ convSExp "return" good n
267+
245268iputStrLn :: String -> Idris ()
246−iputStrLn = liftIO . putStrLn
269+iputStrLn s = do i <- getIState
270+ case idris_outputmode i of
271+ RawOutput -> liftIO $ putStrLn s
272+ IdeSlave n ->
273+ case span (/=':') s of
274+ (fn, ':':rest) -> case span isDigit rest of
275+ ([], ':':msg) -> iWarn (FC fn 0) msg
276+ ([], msg) -> iWarn (FC fn 0) msg
277+ (num, ':':msg) -> iWarn (FC fn (read num)) msg
278+ _ -> liftIO $ putStrLn $ convSExp "write-string" s n
247279
248280iWarn :: FC -> String -> Idris ()
249−iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
281+iWarn fc err = do i <- getIState
282+ case idris_outputmode i of
283+ RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)
284+ IdeSlave n -> liftIO $ putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
250285
251286setLogLevel :: Int -> Idris ()
252287setLogLevel l = do i <- getIState
@@ -323,6 +358,11 @@ outputTy :: Idris OutputType
323358outputTy = do i <- getIState
324359 return $ opt_outputTy $ idris_options i
325360
361+setIdeSlave :: Bool -> Idris ()
362+setIdeSlave True = do i <- getIState
363+ putIState $ i { idris_outputmode = (IdeSlave 0) }
364+setIdeSlave False = return ()
365+
326366verbose :: Idris Bool
327367verbose = do i <- getIState
328368 return (opt_verbose (idris_options i))
src/Idris/AbsSyntaxTree.hs+8−2
@@ -45,6 +45,9 @@ defaultOpts = IOption 0 False False True False False True True False ViaC Execut
4545
4646data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)
4747
48+-- | The output mode in use
49+data OutputMode = RawOutput | IdeSlave Integer deriving Show
50+
4851-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
4952-- without typechecking).
5053-- This will include all the functions and data declarations, plus fixity declarations
@@ -92,7 +95,8 @@ data IState = IState {
9295 ibc_write :: [IBCWrite],
9396 compiled_so :: Maybe String,
9497 idris_dynamic_libs :: [DynamicLib],
95− idris_language_extensions :: [LanguageExt]
98+ idris_language_extensions :: [LanguageExt],
99+ idris_outputmode :: OutputMode
96100 }
97101
98102data SizeChange = Smaller | Same | Bigger | Unknown
@@ -144,10 +148,11 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
144148 emptyContext emptyContext emptyContext emptyContext
145149 emptyContext emptyContext emptyContext emptyContext
146150 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
147− [] Nothing Nothing [] [] [] Hidden False [] Nothing [] []
151+ [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
148152
149153-- | The monad for the main REPL - reading and processing files and updating
150154-- global state (hence the IO inner monad).
155+--type Idris = WriterT [Either String (IO ())] (State IState a))
151156type Idris = StateT IState IO
152157
153158-- Commands in the REPL
@@ -202,6 +207,7 @@ data Opt = Filename String
202207 | Ver
203208 | Usage
204209 | Quiet
210+ | Ideslave
205211 | ShowLibs
206212 | ShowLibdir
207213 | ShowIncs
src/Idris/IdeSlave.hsnew file+126
@@ -0,0 +1,126 @@
1+{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}
2+
3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..)) where
4+
5+import Text.Printf
6+import Numeric
7+import Data.List
8+-- import qualified Data.Text as T
9+import Text.Parsec
10+
11+data SExp = List [SExp]
12+ | StringAtom String
13+ | BoolAtom Bool
14+ | IntegerAtom Integer
15+ | SymbolAtom String
16+ deriving ( Eq, Show )
17+
18+sExpToString :: SExp -> String
19+sExpToString (StringAtom s) = "\"" ++ escape s ++ "\""
20+sExpToString (BoolAtom True) = ":True"
21+sExpToString (BoolAtom False) = ":False"
22+sExpToString (IntegerAtom i) = printf "%d" i
23+sExpToString (SymbolAtom s) = ":" ++ s
24+sExpToString (List l) = "(" ++ intercalate " " (map sExpToString l) ++ ")"
25+
26+class SExpable a where
27+ toSExp :: a -> SExp
28+
29+instance SExpable SExp where
30+ toSExp a = a
31+
32+instance SExpable () where
33+ toSExp a = List [ StringAtom "Unit" ]
34+
35+instance SExpable Bool where
36+ toSExp True = BoolAtom True
37+ toSExp False = BoolAtom False
38+
39+instance SExpable String where
40+ toSExp s = StringAtom s
41+
42+instance SExpable Integer where
43+ toSExp n = IntegerAtom n
44+
45+instance SExpable Int where
46+ toSExp n = IntegerAtom (toInteger n)
47+
48+instance (SExpable a) => SExpable (Maybe a) where
49+ toSExp Nothing = List [SymbolAtom "Nothing"]
50+ toSExp (Just a) = List [SymbolAtom "Just", toSExp a]
51+
52+instance (SExpable a) => SExpable [a] where
53+ toSExp l = List (map toSExp l)
54+
55+instance (SExpable a, SExpable b) => SExpable (a, b) where
56+ toSExp (l, r) = List [toSExp l, toSExp r]
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+
61+escape :: String -> String
62+escape = concatMap escapeChar
63+ where
64+ escapeChar '\\' = "\\\\"
65+ escapeChar '"' = "\\\""
66+ escapeChar c = [c]
67+
68+pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
69+ return (List xs)
70+ <|> atom
71+
72+atom = do char ':'; x <- atomC; return x
73+ <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
74+ <|> do ints <- many1 digit
75+ case readDec ints of
76+ ((num, ""):_) -> return (IntegerAtom (toInteger num))
77+ _ -> return (StringAtom ints)
78+
79+atomC = do string "True"; return (BoolAtom True)
80+ <|> do string "False"; return (BoolAtom False)
81+ <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
82+
83+quotedChar = try (string "\\\\" >> return '\\')
84+ <|> try (string "\\\"" >> return '"')
85+ <|> noneOf "\""
86+
87+parseSExp :: String -> Either ParseError SExp
88+parseSExp = parse pSExp "(unknown)"
89+
90+data IdeSlaveCommand = REPLCompletions String
91+ | Interpret String
92+ | LoadFile String
93+ deriving Show
94+
95+sexpToCommand :: SExp -> Maybe IdeSlaveCommand
96+sexpToCommand (List (x:[])) = sexpToCommand x
97+sexpToCommand (List [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
98+sexpToCommand (List [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
99+sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)
100+sexpToCommand _ = Nothing
101+
102+parseMessage :: String -> (SExp, Integer)
103+parseMessage x = case receiveString x of
104+ (List [cmd, (IntegerAtom id)]) ->
105+ (cmd, id)
106+
107+receiveString :: String -> SExp
108+receiveString x =
109+ case readHex (take 6 x) of
110+ ((num, ""):_) ->
111+ let msg = drop 6 x in
112+ if (length msg) /= (num - 1)
113+ then error "bad input length"
114+ else (case parseSExp msg of
115+ Left _ -> error "parse failure"
116+ Right r -> r)
117+ _ -> error "readHex failed"
118+
119+convSExp :: SExpable a => String -> a -> Integer -> String
120+convSExp pre s id =
121+ let sex = List [SymbolAtom pre, toSExp s, IntegerAtom id] in
122+ let str = sExpToString sex in
123+ (getHexLength str) ++ str
124+
125+getHexLength :: String -> String
126+getHexLength s = printf "%06x" (1 + (length s))
src/Idris/REPL.hs+159−54
@@ -18,6 +18,7 @@ import Idris.UnusedArgs
1818import Idris.Docs
1919import Idris.Help
2020import Idris.Completion
21+import Idris.IdeSlave
2122
2223import Paths_idris
2324import Util.System
@@ -80,6 +81,104 @@ repl orig mods
8081 ctrlC e = do lift $ iputStrLn (show e)
8182 repl orig mods
8283
84+-- | Run the IdeSlave
85+ideslaveStart :: IState -> [FilePath] -> Idris ()
86+ideslaveStart orig mods
87+ = do i <- getIState
88+ case idris_outputmode i of
89+ IdeSlave n ->
90+ when (mods /= []) (do liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt mods) n)
91+ ideslave orig mods
92+
93+
94+ideslave :: IState -> [FilePath] -> Idris ()
95+ideslave orig mods
96+ = do idrisCatch
97+ (do l <- liftIO $ getLine
98+ let (sexp, id) = parseMessage l
99+ i <- getIState
100+ putIState $ i { idris_outputmode = (IdeSlave id) }
101+ case sexpToCommand sexp of
102+ Just (Interpret cmd) ->
103+ do let fn = case mods of
104+ (f:_) -> f
105+ _ -> ""
106+ case parseCmd i cmd of
107+ Left err -> iFail $ show err
108+ Right cmd -> idrisCatch
109+ (do ideslaveProcess fn cmd)
110+ (\e -> do iFail $ show e)
111+ Just (REPLCompletions str) ->
112+ do (unused, compls) <- replCompletion (reverse str, "")
113+ let good = List [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
114+ liftIO $ putStrLn $ convSExp "return" good id
115+ Just (LoadFile filename) ->
116+ do clearErr
117+ putIState (orig { idris_options = idris_options i,
118+ idris_outputmode = (IdeSlave id) })
119+ loadModule filename
120+ iucheck
121+ liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id
122+ -- report success! or failure!
123+ ideslave orig [filename]
124+ Nothing -> do iFail "did not understand")
125+ (\e -> do iFail $ show e)
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+
181+
83182-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
84183mkPrompt [] = "Idris"
85184mkPrompt [x] = "*" ++ dropExtension x
@@ -173,25 +272,25 @@ proofs orig
173272
174273insertScript :: String -> [String] -> [String]
175274insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
176−insertScript prf (p@"---------- Proofs ----------" : "" : xs)
275+insertScript prf (p@"---------- Proofs ----------" : "" : xs)
177276 = p : "" : prf : xs
178277insertScript prf (x : xs) = x : insertScript prf xs
179278
180279process :: FilePath -> Command -> Idris ()
181−process fn Help = iputStrLn displayHelp
280+process fn Help = iResult displayHelp
182281process fn (ChangeDirectory f)
183282 = do liftIO $ setCurrentDirectory f
184283 return ()
185−process fn (Eval t)
284+process fn (Eval t)
186285 = do (tm, ty) <- elabVal toplevel False t
187286 ctxt <- getContext
188− ist <- getIState
287+ ist <- getIState
189288 let tm' = normaliseAll ctxt [] tm
190289 let ty' = normaliseAll ctxt [] ty
191290 logLvl 3 $ "Raw: " ++ show (tm', ty')
192291 imp <- impShow
193− iputStrLn (showImp imp (delab ist tm') ++ " : " ++
194− showImp imp (delab ist ty'))
292+ iResult (showImp imp (delab ist tm') ++ " : " ++
293+ showImp imp (delab ist ty'))
195294process fn (ExecVal t)
196295 = do ctxt <- getContext
197296 ist <- getIState
@@ -200,30 +299,31 @@ process fn (ExecVal t)
200299 let ty' = normaliseAll ctxt [] ty
201300 res <- execute tm
202301 imp <- impShow
203− iputStrLn (showImp imp (delab ist res) ++ " : " ++
204− showImp imp (delab ist ty'))
205− return ()
302+ iResult (showImp imp (delab ist res) ++ " : " ++
303+ showImp imp (delab ist ty'))
206304process fn (Check (PRef _ n))
207305 = do ctxt <- getContext
208306 ist <- getIState
209307 imp <- impShow
210308 case lookupNames n ctxt of
211− ts@(_:_) -> mapM_ (\n -> iputStrLn $ show n ++ " : " ++
212− showImp imp (delabTy ist n)) ts
213− [] -> iputStrLn $ "No such variable " ++ show n
309+ ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++
310+ showImp imp (delabTy ist n)) ts
311+ iResult ""
312+ [] -> iFail $ "No such variable " ++ show n
214313process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
215314 ctxt <- getContext
216− ist <- getIState
315+ ist <- getIState
217316 imp <- impShow
218317 let ty' = normaliseC ctxt [] ty
219− iputStrLn (showImp imp (delab ist tm) ++ " : " ++
220− showImp imp (delab ist ty))
318+ iResult (showImp imp (delab ist tm) ++ " : " ++
319+ showImp imp (delab ist ty))
221320
222321process fn (DocStr n) = do i <- getIState
223322 case lookupCtxtName n (idris_docstrings i) of
224− [] -> iputStrLn $ "No documentation for " ++ show n
225− ns -> mapM_ showDoc ns
226− where showDoc (n, d)
323+ [] -> iFail $ "No documentation for " ++ show n
324+ ns -> do mapM_ showDoc ns
325+ iResult ""
326+ where showDoc (n, d)
227327 = do doc <- getDocs n
228328 iputStrLn $ show doc
229329process fn Universes = do i <- getIState
@@ -233,8 +333,8 @@ process fn Universes = do i <- getIState
233333 let n = length cs
234334 iputStrLn $ "(" ++ show n ++ " constraints)"
235335 case ucheck cs of
236− Error e -> iputStrLn $ pshow i e
237− OK _ -> iputStrLn "Universes OK"
336+ Error e -> iFail $ pshow i e
337+ OK _ -> iResult "Universes OK"
238338process fn (Defn n) = do i <- getIState
239339 iputStrLn "Compiled patterns:\n"
240340 liftIO $ print (lookupDef n (tt_ctxt i))
@@ -245,15 +345,15 @@ process fn (Defn n) = do i <- getIState
245345 case lookupTotal n (tt_ctxt i) of
246346 [t] -> iputStrLn (showTotal t i)
247347 _ -> return ()
248− where printCase i (_, lhs, rhs)
249− = do liftIO $ putStr $ showImp True (delab i lhs)
250− liftIO $ putStr " = "
251− liftIO $ putStrLn $ showImp True (delab i rhs)
348+ where printCase i (_, lhs, rhs)
349+ = do iputStrLn (showImp True (delab i lhs) ++ " = " ++
350+ showImp True (delab i rhs))
252351process fn (TotCheck n) = do i <- getIState
253352 case lookupTotal n (tt_ctxt i) of
254− [t] -> iputStrLn (showTotal t i)
255− _ -> return ()
256−process fn (DebugInfo n)
353+ [t] -> iResult (showTotal t i)
354+ _ -> do iFail ""
355+ return ()
356+process fn (DebugInfo n)
257357 = do i <- getIState
258358 let oi = lookupCtxtName n (idris_optimisation i)
259359 when (not (null oi)) $ iputStrLn (show oi)
@@ -275,13 +375,13 @@ process fn (DebugInfo n)
275375process fn (Info n) = do i <- getIState
276376 case lookupCtxt n (idris_classes i) of
277377 [c] -> classInfo c
278− _ -> iputStrLn "Not a class"
279−process fn (Search t) = iputStrLn "Not implemented"
378+ _ -> iFail "Not a class"
379+process fn (Search t) = iFail "Not implemented"
280380process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
281381 ctxt <- getContext
282382 ist <- getIState
283383 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
284− iputStrLn (show (delab ist tm'))
384+ iResult (show (delab ist tm'))
285385
286386process fn (RmProof n')
287387 = do i <- getIState
@@ -333,8 +433,8 @@ process fn (ShowProof n')
333433 n <- resolveProof n'
334434 let proofs = proof_list i
335435 case lookup n proofs of
336− Nothing -> iputStrLn "No proof to show"
337− Just p -> iputStrLn $ showProof False n p
436+ Nothing -> iFail "No proof to show"
437+ Just p -> iResult $ showProof False n p
338438
339439process fn (Prove n')
340440 = do ctxt <- getContext
@@ -354,13 +454,13 @@ process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
354454 ctxt <- getContext
355455 ist <- getIState
356456 let tm' = hnf ctxt [] tm
357− iputStrLn (show (delab ist tm'))
457+ iResult (show (delab ist tm'))
358458process fn TTShell = do ist <- getIState
359459 let shst = initState (tt_ctxt ist)
360460 runShell shst
361461 return ()
362−process fn Execute = do (m, _) <- elabVal toplevel False
363− (PApp fc
462+process fn Execute = do (m, _) <- elabVal toplevel False
463+ (PApp fc
364464 (PRef fc (UN "run__IO"))
365465 [pexp $ PRef fc (NS (UN "main") ["Main"])])
366466-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
@@ -370,37 +470,37 @@ process fn Execute = do (m, _) <- elabVal toplevel False
370470 compile t tmpn m
371471 liftIO $ system tmpn
372472 return ()
373− where fc = FC "main" 0
374−process fn (NewCompile f)
473+ where fc = FC "main" 0
474+process fn (NewCompile f)
375475 = do (m, _) <- elabVal toplevel False
376476 (PApp fc (PRef fc (UN "run__IO"))
377477 [pexp $ PRef fc (NS (UN "main") ["Main"])])
378478 compileEpic f m
379− where fc = FC "main" 0
380−process fn (Compile target f)
479+ where fc = FC "main" 0
480+process fn (Compile target f)
381481 = do (m, _) <- elabVal toplevel False
382482 (PApp fc (PRef fc (UN "run__IO"))
383483 [pexp $ PRef fc (NS (UN "main") ["Main"])])
384484 compile target f m
385− where fc = FC "main" 0
386−process fn (LogLvl i) = setLogLevel i
485+ where fc = FC "main" 0
486+process fn (LogLvl i) = setLogLevel i
387487-- Elaborate as if LHS of a pattern (debug command)
388−process fn (Pattelab t)
488+process fn (Pattelab t)
389489 = do (tm, ty) <- elabVal toplevel True t
390− iputStrLn $ show tm ++ "\n\n : " ++ show ty
490+ iResult $ show tm ++ "\n\n : " ++ show ty
391491
392−process fn (Missing n)
492+process fn (Missing n)
393493 = do i <- getIState
394494 case lookupCtxt n (idris_patdefs i) of
395495 [] -> return ()
396− [(_, tms)] ->
397− iputStrLn (showSep "\n" (map (showImp True) tms))
398− _ -> iputStrLn $ "Ambiguous name"
496+ [(_, tms)] ->
497+ iResult (showSep "\n" (map (showImp True) tms))
498+ _ -> iFail $ "Ambiguous name"
399499process fn (DynamicLink l) = do i <- getIState
400500 let lib = trim l
401501 handle <- lift $ tryLoadLib lib
402502 case handle of
403− Nothing -> iputStrLn $ "Could not load dynamic lib \"" ++ l ++ "\""
503+ Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""
404504 Just x -> do let libs = idris_dynamic_libs i
405505 putIState $ i { idris_dynamic_libs = x:libs }
406506 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
@@ -413,8 +513,8 @@ process fn Metavars
413513 = do ist <- getIState
414514 let mvs = idris_metavars ist \\ primDefs
415515 case mvs of
416− [] -> iputStrLn "No global metavariables to solve"
417− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
516+ [] -> iFail "No global metavariables to solve"
517+ _ -> iResult $ "Global metavariables:\n\t" ++ show mvs
418518process fn NOP = return ()
419519
420520process fn (SetOpt ErrContext) = setErrContext True
@@ -422,8 +522,8 @@ process fn (UnsetOpt ErrContext) = setErrContext False
422522process fn (SetOpt ShowImpl) = setImpShow True
423523process fn (UnsetOpt ShowImpl) = setImpShow False
424524
425−process fn (SetOpt _) = iputStrLn "Not a valid option"
426−process fn (UnsetOpt _) = iputStrLn "Not a valid option"
525+process fn (SetOpt _) = iFail "Not a valid option"
526+process fn (UnsetOpt _) = iFail "Not a valid option"
427527
428528
429529classInfo :: ClassInfo -> Idris ()
@@ -432,6 +532,7 @@ classInfo ci = do iputStrLn "Methods:\n"
432532 iputStrLn ""
433533 iputStrLn "Instances:\n"
434534 mapM_ dumpInstance (class_instances ci)
535+ iResult ""
435536
436537dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
437538dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
@@ -471,6 +572,7 @@ parseTarget _ = error "unknown target" -- FIXME: partial function
471572parseArgs :: [String] -> [Opt]
472573parseArgs [] = []
473574parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
575+parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
474576parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
475577parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
476578parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
@@ -524,6 +626,7 @@ idrisMain :: [Opt] -> Idris ()
524626idrisMain opts =
525627 do let inputs = opt getFile opts
526628 let quiet = Quiet `elem` opts
629+ let idesl = Ideslave `elem` opts
527630 let runrepl = not (NoREPL `elem` opts)
528631 let output = opt getOutput opts
529632 let newoutput = opt getNewOutput opts
@@ -543,6 +646,7 @@ idrisMain opts =
543646 mapM_ addLangExt (opt getLanguageExt opts)
544647 setREPL runrepl
545648 setQuiet quiet
649+ setIdeSlave idesl
546650 setVerbose runrepl
547651 setCmdLine opts
548652 setOutputTy outty
@@ -567,7 +671,7 @@ idrisMain opts =
567671 elabPrims
568672 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
569673 return ()
570− when (runrepl && not quiet) $ iputStrLn banner
674+ when (runrepl && not quiet && not idesl) $ iputStrLn banner
571675 ist <- getIState
572676 mods <- mapM loadModule inputs
573677 ok <- noErrors
@@ -577,7 +681,8 @@ idrisMain opts =
577681 when ok $ case newoutput of
578682 [] -> return ()
579683 (o:_) -> process "" (NewCompile o)
580− when runrepl $ runInputT replSettings $ repl ist inputs
684+ when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
685+ when (idesl) $ ideslaveStart ist inputs
581686 ok <- noErrors
582687 when (not ok) $ liftIO (exitWith (ExitFailure 1))
583688 where