d20f35c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add --client option

d20f35cEdwin Brady13 years ago

idris.cabal+2−1

compare with master

unifiedsplit

@@ -390,6 +390,7 @@ Executable idris

390 , utf8-string

391 , vector

392 , vector-binary-instances

393+ , network

393

394

394 Extensions: MultiParamTypeClasses

395 Extensions: MultiParamTypeClasses

395 , FunctionalDependencies

396 , FunctionalDependencies

@@ -397,7 +398,7 @@ Executable idris

397 , TemplateHaskell

398 , TemplateHaskell

398

399

399 ghc-prof-options: -auto-all -caf-all

400 ghc-prof-options: -auto-all -caf-all

400− ghc-options: -rtsopts

401+ ghc-options: -threaded -rtsopts

401

402

402 if os(linux)

403 if os(linux)

403 cpp-options: -DLINUX

404 cpp-options: -DLINUX

src/Idris/AbsSyntax.hs+43−33

@@ -16,6 +16,7 @@ import Util.DynamicLinker

16import Paths_idris

18import System.Console.Haskeline

19+import System.IO

20import Control.Monad.State

21import Control.Monad.State

@@ -244,6 +245,7 @@ getInternalApp :: FilePath -> Int -> Idris PTerm

244getInternalApp fp l = do i <- getIState

245getInternalApp fp l = do i <- getIState

245 case lookup (fp, l) (idris_lineapps i) of

246 case lookup (fp, l) (idris_lineapps i) of

246 Just n' -> return n'

247 Just n' -> return n'

248+ Nothing -> return Placeholder

247 -- TODO: What if it's not there?

249 -- TODO: What if it's not there?

248

250

249checkUndefined :: FC -> Name -> Idris ()

251checkUndefined :: FC -> Name -> Idris ()

@@ -296,41 +298,45 @@ solveDeferred :: Name -> Idris ()

296solveDeferred n = do i <- getIState

298solveDeferred n = do i <- getIState

297 putIState $ i { idris_metavars = idris_metavars i \\ [n] }

299 putIState $ i { idris_metavars = idris_metavars i \\ [n] }

298

300

301+ihPrintResult :: Handle -> String -> Idris ()

302+ihPrintResult h s = do i <- getIState

303+ case idris_outputmode i of

304+ RawOutput -> case s of

305+ "" -> return ()

306+ s -> runIO $ hPutStrLn h s

307+ IdeSlave n ->

308+ let good = SexpList [SymbolAtom "ok", toSExp s] in

309+ runIO $ hPutStrLn h $ convSExp "return" good n

310+

311+ihPrintError :: Handle -> String -> Idris ()

312+ihPrintError h s = do i <- getIState

313+ case idris_outputmode i of

314+ RawOutput -> case s of

315+ "" -> return ()

316+ s -> runIO $ hPutStrLn h s

317+ IdeSlave n ->

318+ let good = SexpList [SymbolAtom "error", toSExp s] in

319+ runIO . hPutStrLn h $ convSExp "return" good n

320+

299−iPrintResult :: String -> Idris ()

321+ihputStrLn :: Handle -> String -> Idris ()

300−iPrintResult s = do i <- getIState

322+ihputStrLn h s = do i <- getIState

301 case idris_outputmode i of

323 case idris_outputmode i of

302− RawOutput -> case s of

324+ RawOutput -> runIO $ hPutStrLn h s

303− "" -> return ()

304− s -> runIO $ putStrLn s

305 IdeSlave n ->

325 IdeSlave n ->

306− let good = SexpList [SymbolAtom "ok", toSExp s] in

307− runIO $ putStrLn $ convSExp "return" good n

308−

309−iPrintError :: String -> Idris ()

310−iPrintError s = do i <- getIState

311− case idris_outputmode i of

312− RawOutput -> case s of

313− "" -> return ()

314− s -> runIO $ putStrLn s

315− IdeSlave n ->

316− let good = SexpList [SymbolAtom "error", toSExp s] in

317− runIO . putStrLn $ convSExp "return" good n

318−

319−iputStrLn :: String -> Idris ()

320−iputStrLn s = do i <- getIState

321− case idris_outputmode i of

322− RawOutput -> runIO $ putStrLn s

323− IdeSlave n ->

324− case span (/=':') s of

326+ case span (/=':') s of

325− (fn, ':':rest) -> case span isDigit rest of

327+ (fn, ':':rest) -> case span isDigit rest of

326− ([], ':':msg) -> write

328+ ([], ':':msg) -> write

327− ([], msg) -> write

329+ ([], msg) -> write

328− (row, ':':rest') ->

330+ (row, ':':rest') ->

329− case span isDigit rest' of

331+ case span isDigit rest' of

330− ([], msg) -> iWarn (FC fn (read row) 0) msg

332+ ([], msg) -> iWarn (FC fn (read row) 0) msg

331− (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg

333+ (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg

332− _ -> write

334+ _ -> write

333− where write = runIO . putStrLn $ convSExp "write-string" s n

335+ where write = runIO . hPutStrLn h $ convSExp "write-string" s n

336+

337+iputStrLn = ihputStrLn stdout

338+iPrintError = ihPrintError stdout

339+iPrintResult = ihPrintResult stdout

334

340

335ideslavePutSExp :: SExpable a => String -> a -> Idris ()

341ideslavePutSExp :: SExpable a => String -> a -> Idris ()

336ideslavePutSExp cmd info = do i <- getIState

342ideslavePutSExp cmd info = do i <- getIState

@@ -539,6 +545,10 @@ setColourise :: Bool -> Idris ()

539setColourise b = do i <- getIState

545setColourise b = do i <- getIState

540 putIState $ i { idris_colourRepl = b }

546 putIState $ i { idris_colourRepl = b }

541

547

548+setOutH :: Handle -> Idris ()

549+setOutH h = do i <- getIState

550+ putIState $ i { idris_outh = h }

551+

542impShow :: Idris Bool

552impShow :: Idris Bool

543impShow = do i <- getIState

553impShow = do i <- getIState

544 return (opt_showimp (idris_options i))

554 return (opt_showimp (idris_options i))

src/Idris/AbsSyntaxTree.hs+6−4

@@ -17,7 +17,7 @@ import Idris.Colours

17import Paths_idris

19import System.Console.Haskeline

20−

20+import System.IO

22import Control.Monad.Trans.State.Strict

23import Control.Monad.Trans.Error

@@ -127,7 +127,8 @@ data IState = IState {

127 idris_language_extensions :: [LanguageExt],

128 idris_outputmode :: OutputMode,

129 idris_colourRepl :: Bool,

130− idris_colourTheme :: ColourTheme

130+ idris_colourTheme :: ColourTheme,

131+ idris_outh :: Handle

131 }

132 }

132

133

133data SizeChange = Smaller | Same | Bigger | Unknown

134data SizeChange = Smaller | Same | Bigger | Unknown

@@ -186,7 +187,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

186 emptyContext emptyContext emptyContext emptyContext

187 emptyContext emptyContext emptyContext emptyContext

187 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

188 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

188 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

189 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

189− True defaultTheme

190+ True defaultTheme stdout

190

191

191-- | The monad for the main REPL - reading and processing files and updating

192-- | The monad for the main REPL - reading and processing files and updating

192-- global state (hence the IO inner monad).

193-- global state (hence the IO inner monad).

@@ -239,7 +240,7 @@ data Command = Quit

239 | DebugInfo Name

240 | DebugInfo Name

240 | Search PTerm

241 | Search PTerm

241 | CaseSplit Name PTerm

242 | CaseSplit Name PTerm

242− | CaseSplitAt Int Name

243+ | CaseSplitAt Bool Int Name

243 | SetOpt Opt

244 | SetOpt Opt

244 | UnsetOpt Opt

245 | UnsetOpt Opt

245 | NOP

246 | NOP

@@ -287,6 +288,7 @@ data Opt = Filename String

287 | TargetTriple String

288 | TargetTriple String

288 | TargetCPU String

289 | TargetCPU String

289 | OptLevel Word

290 | OptLevel Word

291+ | Client String

290 deriving (Show, Eq)

292 deriving (Show, Eq)

291

293

292-- Parsed declarations

294-- Parsed declarations

src/Idris/CaseSplit.hs+1−1

@@ -189,7 +189,7 @@ splitOnLine l n fn = do

189replaceSplits :: String -> [[(Name, PTerm)]] -> [String]

190replaceSplits l ups = map (rep (expandBraces l)) ups

191 where

192− rep str [] = str

192+ rep str [] = str ++ "\n"

193 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups

194

195 -- TMP HACK: If there are Nats, we don't want to show as numerals since

src/Idris/ElabDecls.hs+2−1

@@ -1490,7 +1490,8 @@ elabDecl what info d

1490 = idrisCatch (elabDecl' what info d)

1491 (\e -> do setErrLine (getErrLine e)

1492 ist <- getIState

1493+ let h = idris_outh ist

1493− iputStrLn $ pshow ist e)

1494+ ihputStrLn h $ pshow ist e)

1494

1495

1495elabDecl' _ info (PFix _ _ _)

1496elabDecl' _ info (PFix _ _ _)

1496 = return () -- nothing to elaborate

1497 = return () -- nothing to elaborate

src/Idris/Parser.hs+22−20

@@ -54,6 +54,8 @@ import qualified Data.ByteString.UTF8 as UTF8

54import Debug.Trace

56import System.FilePath

57+import System.IO

58+

57{-

59{-

58 grammar shortcut notation:

60 grammar shortcut notation:

59 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)

61 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)

@@ -902,10 +904,10 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

902parseProg syn fname input mrk

904parseProg syn fname input mrk

903 = do i <- getIState

905 = do i <- getIState

904 case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

906 case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

905− Failure doc -> do iputStrLn (show doc)

906− -- FIXME: Get error location from trifecta

907+ Failure doc -> do -- FIXME: Get error location from trifecta

907 --let errl = sourceLine (errorPos err)

908 --let errl = sourceLine (errorPos err)

908 i <- getIState

909 i <- getIState

910+ ihputStrLn (idris_outh i) (show doc)

909 putIState (i { errLine = Just 0 }) -- Just errl })

911 putIState (i { errLine = Just 0 }) -- Just errl })

910 return []

912 return []

911 Success (x, i) -> do putIState i

913 Success (x, i) -> do putIState i

@@ -920,8 +922,8 @@ parseProg syn fname input mrk

920 return (ds, i')

922 return (ds, i')

921

923

922{- | Load idris module -}

924{- | Load idris module -}

923−loadModule :: FilePath -> Idris String

925+loadModule :: Handle -> FilePath -> Idris String

924−loadModule f

926+loadModule outh f

925 = idrisCatch (do i <- getIState

927 = idrisCatch (do i <- getIState

926 let file = takeWhile (/= ' ') f

928 let file = takeWhile (/= ' ') f

927 ibcsd <- valIBCSubDir i

929 ibcsd <- valIBCSubDir i

@@ -931,25 +933,25 @@ loadModule f

931 then iLOG $ "Already read " ++ file

933 then iLOG $ "Already read " ++ file

932 else do putIState (i { imported = file : imported i })

934 else do putIState (i { imported = file : imported i })

933 case fp of

935 case fp of

934− IDR fn -> loadSource False fn

936+ IDR fn -> loadSource outh False fn

935− LIDR fn -> loadSource True fn

937+ LIDR fn -> loadSource outh True fn

936 IBC fn src ->

938 IBC fn src ->

937 idrisCatch (loadIBC fn)

939 idrisCatch (loadIBC fn)

938 (\c -> do iLOG $ fn ++ " failed " ++ show c

940 (\c -> do iLOG $ fn ++ " failed " ++ show c

939 case src of

941 case src of

940− IDR sfn -> loadSource False sfn

942+ IDR sfn -> loadSource outh False sfn

941− LIDR sfn -> loadSource True sfn)

943+ LIDR sfn -> loadSource outh True sfn)

942 let (dir, fh) = splitFileName file

944 let (dir, fh) = splitFileName file

943 return (dropExtension fh))

945 return (dropExtension fh))

944 (\e -> do setErrLine (getErrLine e)

946 (\e -> do setErrLine (getErrLine e)

945 ist <- getIState

947 ist <- getIState

946 msg <- showErr e

948 msg <- showErr e

947− iputStrLn msg

949+ ihputStrLn outh msg

948 return "")

950 return "")

949

951

950{- | Load idris code from file -}

952{- | Load idris code from file -}

951−loadFromIFile :: IFileType -> Idris ()

953+loadFromIFile :: Handle -> IFileType -> Idris ()

952−loadFromIFile i@(IBC fn src)

954+loadFromIFile h i@(IBC fn src)

953 = do iLOG $ "Skipping " ++ getSrcFile i

955 = do iLOG $ "Skipping " ++ getSrcFile i

954 idrisCatch (loadIBC fn)

956 idrisCatch (loadIBC fn)

955 (\err -> ierror $ LoadingFailed fn err)

957 (\err -> ierror $ LoadingFailed fn err)

@@ -958,20 +960,20 @@ loadFromIFile i@(IBC fn src)

958 getSrcFile (LIDR fn) = fn

960 getSrcFile (LIDR fn) = fn

959 getSrcFile (IBC f src) = getSrcFile src

961 getSrcFile (IBC f src) = getSrcFile src

960

962

961−loadFromIFile (IDR fn) = loadSource' False fn

963+loadFromIFile h (IDR fn) = loadSource' h False fn

962−loadFromIFile (LIDR fn) = loadSource' True fn

964+loadFromIFile h (LIDR fn) = loadSource' h True fn

963

965

964{-| Load idris source code and show error if something wrong happens -}

966{-| Load idris source code and show error if something wrong happens -}

965−loadSource' :: Bool -> FilePath -> Idris ()

967+loadSource' :: Handle -> Bool -> FilePath -> Idris ()

966−loadSource' lidr r

968+loadSource' h lidr r

967− = idrisCatch (loadSource lidr r)

969+ = idrisCatch (loadSource h lidr r)

968 (\e -> do setErrLine (getErrLine e)

970 (\e -> do setErrLine (getErrLine e)

969 msg <- showErr e

971 msg <- showErr e

970− iputStrLn msg)

972+ ihputStrLn h msg)

971

973

972{- | Load Idris source code-}

974{- | Load Idris source code-}

973−loadSource :: Bool -> FilePath -> Idris ()

975+loadSource :: Handle -> Bool -> FilePath -> Idris ()

974−loadSource lidr f

976+loadSource h lidr f

975 = do iLOG ("Reading " ++ f)

977 = do iLOG ("Reading " ++ f)

976 i <- getIState

978 i <- getIState

977 let def_total = default_total i

979 let def_total = default_total i

@@ -992,7 +994,7 @@ loadSource lidr f

992 logLvl 3 (show (idris_infixes i))

994 logLvl 3 (show (idris_infixes i))

993 -- Now add all the declarations to the context

995 -- Now add all the declarations to the context

994 v <- verbose

996 v <- verbose

995− when v $ iputStrLn $ "Type checking " ++ f

997+ when v $ ihputStrLn h $ "Type checking " ++ f

996 -- we totality check after every Mutual block, so if

998 -- we totality check after every Mutual block, so if

997 -- anything is a single definition, wrap it in a

999 -- anything is a single definition, wrap it in a

998 -- mutual block on its own

1000 -- mutual block on its own

src/Idris/REPL.hs+197−109

@@ -58,8 +58,11 @@ import System.Directory

58import System.IO

59import Control.Monad

60import Control.Monad.Trans.Error (ErrorT(..))

61−import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )

61+import Control.Monad.Trans.State.Strict ( StateT, execStateT, evalStateT, get, put )

62import Control.Monad.Trans ( lift )

63+import Control.Concurrent.MVar

64+import Network

65+import Control.Concurrent

63import Data.Maybe

66import Data.Maybe

64import Data.List

67import Data.List

65import Data.Char

68import Data.Char

@@ -72,12 +75,14 @@ import Debug.Trace

73-- | Run the REPL

76-- | Run the REPL

74repl :: IState -- ^ The initial state

77repl :: IState -- ^ The initial state

78+ -> MVar IState -- ^ Server's MVar

75 -> [FilePath] -- ^ The loaded modules

79 -> [FilePath] -- ^ The loaded modules

76 -> InputT Idris ()

80 -> InputT Idris ()

77−repl orig mods

81+repl orig stvar mods

78 = H.catch

82 = H.catch

79 (do let quiet = opt_quiet (idris_options orig)

83 (do let quiet = opt_quiet (idris_options orig)

80 i <- lift getIState

84 i <- lift getIState

85+ lift $ runIO $ swapMVar stvar i -- update shared state

81 let colour = idris_colourRepl i

86 let colour = idris_colourRepl i

82 let theme = idris_colourTheme i

87 let theme = idris_colourTheme i

83 let prompt = if quiet

88 let prompt = if quiet

@@ -89,15 +94,74 @@ repl orig mods

89 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

94 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

90 return ()

95 return ()

91 Just input -> H.catch

96 Just input -> H.catch

92− (do ms <- lift $ processInput input orig mods

97+ (do ms <- lift $ processInput stvar input orig mods

93 case ms of

98 case ms of

94− Just mods -> repl orig mods

99+ Just mods -> repl orig stvar mods

95 Nothing -> return ())

100 Nothing -> return ())

96 ctrlC)

101 ctrlC)

97− ctrlC

102+ ctrlC

98 where ctrlC :: SomeException -> InputT Idris ()

103 where ctrlC :: SomeException -> InputT Idris ()

99 ctrlC e = do lift $ iputStrLn (show e)

104 ctrlC e = do lift $ iputStrLn (show e)

100− repl orig mods

105+ repl orig stvar mods

106+

107+-- | Run the REPL server

108+startServer :: IState -> MVar IState -> [FilePath] -> Idris ()

109+startServer orig stvar fn_in = do tid <- runIO $ forkOS serverLoop

110+ return ()

111+ where serverLoop :: IO ()

112+ -- TODO: option for port number

113+ serverLoop = withSocketsDo $ do sock <- listenOn $ PortNumber 4294

114+ i <- readMVar stvar

115+ loop i sock

116+

117+ fn = case fn_in of

118+ (f:_) -> f

119+ _ -> ""

120+

121+ loop ist sock = do (h,_,_) <- accept sock

122+ cmd <- hGetLine h

123+ takeMVar stvar

124+ ist' <- processNetCmd stvar orig ist h fn cmd

125+ putMVar stvar ist'

126+ hClose h

127+ loop ist' sock

128+

129+processNetCmd :: MVar IState ->

130+ IState -> IState -> Handle -> FilePath -> String -> IO IState

131+processNetCmd stvar orig i h fn cmd

132+ = do res <- case parseCmd i "(net)" cmd of

133+ Failure err -> return (Left (Msg " invalid command"))

134+ Success c -> runErrorT $ evalStateT (processNet fn c) i

135+ case res of

136+ Right ist -> return ist

137+ Left err -> do hPutStrLn h (show err)

138+ return i

139+ where

140+ processNet fn Reload =

141+ do let ist = orig { idris_options = idris_options i

142+ , idris_colourTheme = idris_colourTheme i

143+ }

144+ putIState orig

145+ setOutH h

146+ mods <- loadInputs h [fn]

147+ ist <- getIState

148+ return ist

149+ processNet fn c = do process h fn c

150+ ist <- getIState

151+ return ist

152+

153+-- | Run a command on the server on localhost

154+runClient :: String -> IO ()

155+runClient str = withSocketsDo $ do

156+ h <- connectTo "localhost" (PortNumber 4294)

157+ hPutStrLn h str

158+ resp <- hGetResp "" h

159+ putStr resp

160+ hClose h

161+ where hGetResp acc h = do eof <- hIsEOF h

162+ if eof then return acc

163+ else do l <- hGetLine h

164+ hGetResp (acc ++ l ++ "\n") h

101

165

102-- | Run the IdeSlave

166-- | Run the IdeSlave

103ideslaveStart :: IState -> [FilePath] -> Idris ()

167ideslaveStart :: IState -> [FilePath] -> Idris ()

@@ -126,7 +190,7 @@ ideslave orig mods

126 Failure err -> iPrintError $ show (fixColour c err)

190 Failure err -> iPrintError $ show (fixColour c err)

127 Success (Prove n') -> do iPrintResult ""

191 Success (Prove n') -> do iPrintResult ""

128 idrisCatch

192 idrisCatch

129− (process fn (Prove n'))

193+ (process stdout fn (Prove n'))

130 (\e -> getIState >>= iPrintError . flip pshow e)

194 (\e -> getIState >>= iPrintError . flip pshow e)

131 isetPrompt (mkPrompt mods)

195 isetPrompt (mkPrompt mods)

132 Success cmd -> idrisCatch

196 Success cmd -> idrisCatch

@@ -140,7 +204,7 @@ ideslave orig mods

140 do clearErr

204 do clearErr

141 putIState (orig { idris_options = idris_options i,

205 putIState (orig { idris_options = idris_options i,

142 idris_outputmode = (IdeSlave id) })

206 idris_outputmode = (IdeSlave id) })

143− loadModule filename

207+ loadModule stdout filename

144 iucheck

208 iucheck

145 isetPrompt (mkPrompt [filename])

209 isetPrompt (mkPrompt [filename])

146

210

@@ -155,53 +219,53 @@ ideslave orig mods

155 ideslave orig mods

219 ideslave orig mods

156

220

157ideslaveProcess :: FilePath -> Command -> Idris ()

221ideslaveProcess :: FilePath -> Command -> Idris ()

158−ideslaveProcess fn Help = process fn Help

222+ideslaveProcess fn Help = process stdout fn Help

159−ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

223+ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

160 iPrintResult "changed directory to"

224 iPrintResult "changed directory to"

161−ideslaveProcess fn (Eval t) = process fn (Eval t)

225+ideslaveProcess fn (Eval t) = process stdout fn (Eval t)

162−ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)

226+ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)

163−ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

227+ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))

164−ideslaveProcess fn (Check t) = process fn (Check t)

228+ideslaveProcess fn (Check t) = process stdout fn (Check t)

165−ideslaveProcess fn (DocStr n) = process fn (DocStr n)

229+ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)

166−ideslaveProcess fn Universes = process fn Universes

230+ideslaveProcess fn Universes = process stdout fn Universes

167−ideslaveProcess fn (Defn n) = do process fn (Defn n)

231+ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)

168 iPrintResult ""

232 iPrintResult ""

169−ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

233+ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)

170−ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

234+ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)

171 iPrintResult ""

235 iPrintResult ""

172−ideslaveProcess fn (Info n) = process fn (Info n)

236+ideslaveProcess fn (Info n) = process stdout fn (Info n)

173−ideslaveProcess fn (Search t) = process fn (Search t)

237+ideslaveProcess fn (Search t) = process stdout fn (Search t)

174−ideslaveProcess fn (Spec t) = process fn (Spec t)

238+ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

175-- RmProof and AddProof not supported!

239-- RmProof and AddProof not supported!

176−ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

240+ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')

177−ideslaveProcess fn (HNF t) = process fn (HNF t)

241+ideslaveProcess fn (HNF t) = process stdout fn (HNF t)

178−--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!

242+--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!

179

243

180--that most likely does not work, since we need to wrap

244--that most likely does not work, since we need to wrap

181--input/output of the executed binary...

245--input/output of the executed binary...

182−ideslaveProcess fn Execute = do process fn Execute

246+ideslaveProcess fn Execute = do process stdout fn Execute

183 iPrintResult ""

247 iPrintResult ""

184−ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

248+ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)

185 iPrintResult ""

249 iPrintResult ""

186−ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

250+ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)

187 iPrintResult ""

251 iPrintResult ""

188−ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

252+ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)

189−ideslaveProcess fn (Missing n) = process fn (Missing n)

253+ideslaveProcess fn (Missing n) = process stdout fn (Missing n)

190−ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)

254+ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)

191 iPrintResult ""

255 iPrintResult ""

192−ideslaveProcess fn ListDynamic = do process fn ListDynamic

256+ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic

193 iPrintResult ""

257 iPrintResult ""

194−ideslaveProcess fn Metavars = process fn Metavars

258+ideslaveProcess fn Metavars = process stdout fn Metavars

195−ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

259+ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)

196 iPrintResult ""

260 iPrintResult ""

197−ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

261+ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)

198 iPrintResult ""

262 iPrintResult ""

199−ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

263+ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)

200 iPrintResult ""

264 iPrintResult ""

201−ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

265+ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)

202 iPrintResult ""

266 iPrintResult ""

203−ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

267+ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

204−ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

268+ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

205ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

269ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

206

270

207

271

@@ -215,8 +279,9 @@ lit f = case splitExtension f of

215 (_, ".lidr") -> True

279 (_, ".lidr") -> True

216 _ -> False

280 _ -> False

217

281

282+processInput :: MVar IState -> String ->

218−processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])

283+ IState -> [FilePath] -> Idris (Maybe [FilePath])

219−processInput cmd orig inputs

284+processInput stvar cmd orig inputs

220 = do i <- getIState

285 = do i <- getIState

221 let opts = idris_options i

286 let opts = idris_options i

222 let quiet = opt_quiet opts

287 let quiet = opt_quiet opts

@@ -232,26 +297,27 @@ processInput cmd orig inputs

232 , idris_colourTheme = idris_colourTheme i

297 , idris_colourTheme = idris_colourTheme i

233 }

298 }

234 clearErr

299 clearErr

235− mods <- loadInputs inputs

300+ mods <- loadInputs stdout inputs

236 return (Just inputs)

301 return (Just inputs)

237 Success (Load f) ->

302 Success (Load f) ->

238 do putIState orig { idris_options = idris_options i

303 do putIState orig { idris_options = idris_options i

239 , idris_colourTheme = idris_colourTheme i

304 , idris_colourTheme = idris_colourTheme i

240 }

305 }

241 clearErr

306 clearErr

242− mod <- loadModule f

307+ mod <- loadModule stdout f

243 return (Just [f])

308 return (Just [f])

244 Success (ModImport f) ->

309 Success (ModImport f) ->

245 do clearErr

310 do clearErr

246− fmod <- loadModule f

311+ fmod <- loadModule stdout f

247 return (Just (inputs ++ [fmod]))

312 return (Just (inputs ++ [fmod]))

313+ Success Edit -> do -- takeMVar stvar

248− Success Edit -> do edit fn orig

314+ edit fn orig

249 return (Just inputs)

315 return (Just inputs)

250 Success Proofs -> do proofs orig

316 Success Proofs -> do proofs orig

251 return (Just inputs)

317 return (Just inputs)

252 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

318 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

253 return Nothing

319 return Nothing

254− Success cmd -> do idrisCatch (process fn cmd)

320+ Success cmd -> do idrisCatch (process stdout fn cmd)

255 (\e -> do msg <- showErr e ; iputStrLn msg)

321 (\e -> do msg <- showErr e ; iputStrLn msg)

256 return (Just inputs)

322 return (Just inputs)

257

323

@@ -287,7 +353,7 @@ edit f orig

287 putIState $ orig { idris_options = idris_options i

353 putIState $ orig { idris_options = idris_options i

288 , idris_colourTheme = idris_colourTheme i

354 , idris_colourTheme = idris_colourTheme i

289 }

355 }

290− loadInputs [f]

356+ loadInputs stdout [f]

291 iucheck

357 iucheck

292 return ()

358 return ()

293 where getEditor env | Just ed <- lookup "EDITOR" env = ed

359 where getEditor env | Just ed <- lookup "EDITOR" env = ed

@@ -312,12 +378,12 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

312 = p : "" : prf : xs

378 = p : "" : prf : xs

313insertScript prf (x : xs) = x : insertScript prf xs

379insertScript prf (x : xs) = x : insertScript prf xs

314

380

315−process :: FilePath -> Command -> Idris ()

381+process :: Handle -> FilePath -> Command -> Idris ()

316−process fn Help = iPrintResult displayHelp

382+process h fn Help = iPrintResult displayHelp

317−process fn (ChangeDirectory f)

383+process h fn (ChangeDirectory f)

318 = do runIO $ setCurrentDirectory f

384 = do runIO $ setCurrentDirectory f

319 return ()

385 return ()

320−process fn (Eval t)

386+process h fn (Eval t)

321 = do (tm, ty) <- elabVal toplevel False t

387 = do (tm, ty) <- elabVal toplevel False t

322 ctxt <- getContext

388 ctxt <- getContext

323 ist <- getIState

389 ist <- getIState

@@ -329,9 +395,9 @@ process fn (Eval t)

329 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

395 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

330 imp <- impShow

396 imp <- impShow

331 c <- colourise

397 c <- colourise

332− iPrintResult (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

398+ ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

333 showImp (Just ist) imp c (delab ist ty'))

399 showImp (Just ist) imp c (delab ist ty'))

334−process fn (ExecVal t)

400+process h fn (ExecVal t)

335 = do ctxt <- getContext

401 = do ctxt <- getContext

336 ist <- getIState

402 ist <- getIState

337 (tm, ty) <- elabVal toplevel False t

403 (tm, ty) <- elabVal toplevel False t

@@ -340,19 +406,19 @@ process fn (ExecVal t)

340 res <- execute tm

406 res <- execute tm

341 imp <- impShow

407 imp <- impShow

342 c <- colourise

408 c <- colourise

343− iPrintResult (showImp (Just ist) imp c (delab ist res) ++ " : " ++

409+ ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++

344 showImp (Just ist) imp c (delab ist ty'))

410 showImp (Just ist) imp c (delab ist ty'))

345−process fn (Check (PRef _ n))

411+process h fn (Check (PRef _ n))

346 = do ctxt <- getContext

412 = do ctxt <- getContext

347 ist <- getIState

413 ist <- getIState

348 imp <- impShow

414 imp <- impShow

349 c <- colourise

415 c <- colourise

350 case lookupNames n ctxt of

416 case lookupNames n ctxt of

351− ts@(_:_) -> do mapM_ (\n -> iputStrLn $ showName (Just ist) [] False c n ++ " : " ++

417+ ts@(_:_) -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++

352 showImp (Just ist) imp c (delabTy ist n)) ts

418 showImp (Just ist) imp c (delabTy ist n)) ts

353− iPrintResult ""

419+ ihPrintResult h ""

354− [] -> iPrintError $ "No such variable " ++ show n

420+ [] -> ihPrintError h $ "No such variable " ++ show n

355−process fn (Check t)

421+process h fn (Check t)

356 = do (tm, ty) <- elabVal toplevel False t

422 = do (tm, ty) <- elabVal toplevel False t

357 ctxt <- getContext

423 ctxt <- getContext

358 ist <- getIState

424 ist <- getIState

@@ -360,11 +426,12 @@ process fn (Check t)

360 c <- colourise

426 c <- colourise

361 let ty' = normaliseC ctxt [] ty

427 let ty' = normaliseC ctxt [] ty

362 case tm of

428 case tm of

363− TType _ -> iPrintResult ("Type : Type 1")

429+ TType _ -> ihPrintResult h ("Type : Type 1")

364− _ -> iPrintResult (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

430+ _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

365− showImp (Just ist) imp c (delab ist ty))

431+ showImp (Just ist) imp c (delab ist ty))

366

432

367−process fn (DocStr n) = do i <- getIState

433+process h fn (DocStr n)

434+ = do i <- getIState

368 case lookupCtxtName n (idris_docstrings i) of

435 case lookupCtxtName n (idris_docstrings i) of

369 [] -> iPrintError $ "No documentation for " ++ show n

436 [] -> iPrintError $ "No documentation for " ++ show n

370 ns -> do mapM_ showDoc ns

437 ns -> do mapM_ showDoc ns

@@ -372,7 +439,8 @@ process fn (DocStr n) = do i <- getIState

372 where showDoc (n, d)

439 where showDoc (n, d)

373 = do doc <- getDocs n

440 = do doc <- getDocs n

374 iputStrLn $ show doc

441 iputStrLn $ show doc

375−process fn Universes = do i <- getIState

442+process h fn Universes

443+ = do i <- getIState

376 let cs = idris_constraints i

444 let cs = idris_constraints i

377-- iputStrLn $ showSep "\n" (map show cs)

445-- iputStrLn $ showSep "\n" (map show cs)

378 iputStrLn $ show (map fst cs)

446 iputStrLn $ show (map fst cs)

@@ -381,7 +449,8 @@ process fn Universes = do i <- getIState

381 case ucheck cs of

449 case ucheck cs of

382 Error e -> iPrintError $ pshow i e

450 Error e -> iPrintError $ pshow i e

383 OK _ -> iPrintResult "Universes OK"

451 OK _ -> iPrintResult "Universes OK"

384−process fn (Defn n) = do i <- getIState

452+process h fn (Defn n)

453+ = do i <- getIState

385 iputStrLn "Compiled patterns:\n"

454 iputStrLn "Compiled patterns:\n"

386 iputStrLn $ show (lookupDef n (tt_ctxt i))

455 iputStrLn $ show (lookupDef n (tt_ctxt i))

387 case lookupCtxt n (idris_patdefs i) of

456 case lookupCtxt n (idris_patdefs i) of

@@ -395,12 +464,13 @@ process fn (Defn n) = do i <- getIState

395 = do c <- colourise

464 = do c <- colourise

396 iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

465 iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

397 showImp (Just i) True c (delab i rhs))

466 showImp (Just i) True c (delab i rhs))

398−process fn (TotCheck n) = do i <- getIState

467+process h fn (TotCheck n)

468+ = do i <- getIState

399 case lookupTotal n (tt_ctxt i) of

469 case lookupTotal n (tt_ctxt i) of

400 [t] -> iPrintResult (showTotal t i)

470 [t] -> iPrintResult (showTotal t i)

401 _ -> do iPrintError ""

471 _ -> do iPrintError ""

402 return ()

472 return ()

403−process fn (DebugInfo n)

473+process h fn (DebugInfo n)

404 = do i <- getIState

474 = do i <- getIState

405 let oi = lookupCtxtName n (idris_optimisation i)

475 let oi = lookupCtxtName n (idris_optimisation i)

406 when (not (null oi)) $ iputStrLn (show oi)

476 when (not (null oi)) $ iputStrLn (show oi)

@@ -418,29 +488,37 @@ process fn (DebugInfo n)

418 iputStrLn $ "Size change: " ++ show sc

488 iputStrLn $ "Size change: " ++ show sc

419 when (not (null cg')) $ do iputStrLn "Call graph:\n"

489 when (not (null cg')) $ do iputStrLn "Call graph:\n"

420 iputStrLn (show cg')

490 iputStrLn (show cg')

421−process fn (Info n) = do i <- getIState

491+process h fn (Info n)

492+ = do i <- getIState

422 case lookupCtxt n (idris_classes i) of

493 case lookupCtxt n (idris_classes i) of

423 [c] -> classInfo c

494 [c] -> classInfo c

424 _ -> iPrintError "Not a class"

495 _ -> iPrintError "Not a class"

425−process fn (Search t) = iPrintError "Not implemented"

496+process h fn (Search t) = iPrintError "Not implemented"

426−process fn (CaseSplit n t)

497+process h fn (CaseSplit n t)

427 = do tms <- split n t

498 = do tms <- split n t

428 iputStrLn (showSep "\n" (map show tms))

499 iputStrLn (showSep "\n" (map show tms))

429−process fn (CaseSplitAt l n)

500+process h fn (CaseSplitAt updatefile l n)

430 = do src <- runIO $ readFile fn

501 = do src <- runIO $ readFile fn

431 res <- splitOnLine l n fn

502 res <- splitOnLine l n fn

432 iLOG (showSep "\n" (map show res))

503 iLOG (showSep "\n" (map show res))

433 let (before, (ap : later)) = splitAt (l-1) (lines src)

504 let (before, (ap : later)) = splitAt (l-1) (lines src)

434− iputStrLn (showSep "\n" (replaceSplits ap res))

505+ let new = concat (replaceSplits ap res)

506+ ihputStrLn h new

507+ if updatefile then

508+ do let fb = fn ++ "~" -- make a backup!

509+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)

510+ runIO $ copyFile fb fn

511+ else return ()

435

512

436

513

514+process h fn (Spec t)

437−process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

515+ = do (tm, ty) <- elabVal toplevel False t

438 ctxt <- getContext

516 ctxt <- getContext

439 ist <- getIState

517 ist <- getIState

440 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

518 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

441 iPrintResult (show (delab ist tm'))

519 iPrintResult (show (delab ist tm'))

442

520

443−process fn (RmProof n')

521+process h fn (RmProof n')

444 = do i <- getIState

522 = do i <- getIState

445 n <- resolveProof n'

523 n <- resolveProof n'

446 let proofs = proof_list i

524 let proofs = proof_list i

@@ -456,7 +534,7 @@ process fn (RmProof n')

456 let ms = idris_metavars i

534 let ms = idris_metavars i

457 putIState $ i { idris_metavars = n : ms }

535 putIState $ i { idris_metavars = n : ms }

458

536

459−process fn' (AddProof prf)

537+process h fn' (AddProof prf)

460 = do fn <- do

538 = do fn <- do

461 ex <- runIO $ doesFileExist fn'

539 ex <- runIO $ doesFileExist fn'

462 let fnExt = fn' <.> "idr"

540 let fnExt = fn' <.> "idr"

@@ -485,7 +563,7 @@ process fn' (AddProof prf)

485 iputStrLn $ "Added proof " ++ show n

563 iputStrLn $ "Added proof " ++ show n

486 where ls = (lines prog)

564 where ls = (lines prog)

487

565

488−process fn (ShowProof n')

566+process h fn (ShowProof n')

489 = do i <- getIState

567 = do i <- getIState

490 n <- resolveProof n'

568 n <- resolveProof n'

491 let proofs = proof_list i

569 let proofs = proof_list i

@@ -493,7 +571,7 @@ process fn (ShowProof n')

493 Nothing -> iPrintError "No proof to show"

571 Nothing -> iPrintError "No proof to show"

494 Just p -> iPrintResult $ showProof False n p

572 Just p -> iPrintResult $ showProof False n p

495

573

496−process fn (Prove n')

574+process h fn (Prove n')

497 = do ctxt <- getContext

575 = do ctxt <- getContext

498 ist <- getIState

576 ist <- getIState

499 n <- case lookupNames n' ctxt of

577 n <- case lookupNames n' ctxt of

@@ -507,23 +585,27 @@ process fn (Prove n')

507 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

585 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

508 mapM_ checkDeclTotality (idris_totcheck i)

586 mapM_ checkDeclTotality (idris_totcheck i)

509

587

588+process h fn (HNF t)

510−process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

589+ = do (tm, ty) <- elabVal toplevel False t

511 ctxt <- getContext

590 ctxt <- getContext

512 ist <- getIState

591 ist <- getIState

513 let tm' = hnf ctxt [] tm

592 let tm' = hnf ctxt [] tm

514 iPrintResult (show (delab ist tm'))

593 iPrintResult (show (delab ist tm'))

594+process h fn (TestInline t)

515−process fn (TestInline t) = do (tm, ty) <- elabVal toplevel False t

595+ = do (tm, ty) <- elabVal toplevel False t

516 ctxt <- getContext

596 ctxt <- getContext

517 ist <- getIState

597 ist <- getIState

518 let tm' = inlineTerm ist tm

598 let tm' = inlineTerm ist tm

519 imp <- impShow

599 imp <- impShow

520 c <- colourise

600 c <- colourise

521 iPrintResult (showImp (Just ist) imp c (delab ist tm'))

601 iPrintResult (showImp (Just ist) imp c (delab ist tm'))

522−process fn TTShell = do ist <- getIState

602+process h fn TTShell

603+ = do ist <- getIState

523 let shst = initState (tt_ctxt ist)

604 let shst = initState (tt_ctxt ist)

524 runShell shst

605 runShell shst

525 return ()

606 return ()

607+process h fn Execute

526−process fn Execute = do (m, _) <- elabVal toplevel False

608+ = do (m, _) <- elabVal toplevel False

527 (PApp fc

609 (PApp fc

528 (PRef fc (UN "run__IO"))

610 (PRef fc (UN "run__IO"))

529 [pexp $ PRef fc (NS (UN "main") ["Main"])])

611 [pexp $ PRef fc (NS (UN "main") ["Main"])])

@@ -535,19 +617,19 @@ process fn Execute = do (m, _) <- elabVal toplevel False

535 runIO $ system tmpn

617 runIO $ system tmpn

536 return ()

618 return ()

537 where fc = fileFC "main"

619 where fc = fileFC "main"

538−process fn (Compile codegen f)

620+process h fn (Compile codegen f)

539 = do (m, _) <- elabVal toplevel False

621 = do (m, _) <- elabVal toplevel False

540 (PApp fc (PRef fc (UN "run__IO"))

622 (PApp fc (PRef fc (UN "run__IO"))

541 [pexp $ PRef fc (NS (UN "main") ["Main"])])

623 [pexp $ PRef fc (NS (UN "main") ["Main"])])

542 compile codegen f m

624 compile codegen f m

543 where fc = fileFC "main"

625 where fc = fileFC "main"

544−process fn (LogLvl i) = setLogLevel i

626+process h fn (LogLvl i) = setLogLevel i

545-- Elaborate as if LHS of a pattern (debug command)

627-- Elaborate as if LHS of a pattern (debug command)

546−process fn (Pattelab t)

628+process h fn (Pattelab t)

547 = do (tm, ty) <- elabVal toplevel True t

629 = do (tm, ty) <- elabVal toplevel True t

548 iPrintResult $ show tm ++ "\n\n : " ++ show ty

630 iPrintResult $ show tm ++ "\n\n : " ++ show ty

549

631

550−process fn (Missing n)

632+process h fn (Missing n)

551 = do i <- getIState

633 = do i <- getIState

552 c <- colourise

634 c <- colourise

553 case lookupCtxt n (idris_patdefs i) of

635 case lookupCtxt n (idris_patdefs i) of

@@ -555,7 +637,8 @@ process fn (Missing n)

555 [(_, tms)] ->

637 [(_, tms)] ->

556 iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))

638 iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))

557 _ -> iPrintError $ "Ambiguous name"

639 _ -> iPrintError $ "Ambiguous name"

558−process fn (DynamicLink l) = do i <- getIState

640+process h fn (DynamicLink l)

641+ = do i <- getIState

559 let lib = trim l

642 let lib = trim l

560 handle <- lift . lift $ tryLoadLib lib

643 handle <- lift . lift $ tryLoadLib lib

561 case handle of

644 case handle of

@@ -566,33 +649,35 @@ process fn (DynamicLink l) = do i <- getIState

566 return ()

649 return ()

567 else putIState $ i { idris_dynamic_libs = x:libs }

650 else putIState $ i { idris_dynamic_libs = x:libs }

568 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

651 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

569−process fn ListDynamic = do i <- getIState

652+process h fn ListDynamic

653+ = do i <- getIState

570 iputStrLn "Dynamic libraries:"

654 iputStrLn "Dynamic libraries:"

571 showLibs $ idris_dynamic_libs i

655 showLibs $ idris_dynamic_libs i

572 where showLibs [] = return ()

656 where showLibs [] = return ()

573 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

657 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

574−process fn Metavars

658+process h fn Metavars

575 = do ist <- getIState

659 = do ist <- getIState

576 let mvs = idris_metavars ist \\ primDefs

660 let mvs = idris_metavars ist \\ primDefs

577 case mvs of

661 case mvs of

578 [] -> iPrintError "No global metavariables to solve"

662 [] -> iPrintError "No global metavariables to solve"

579 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

663 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

580−process fn NOP = return ()

664+process h fn NOP = return ()

581−

665+

582−process fn (SetOpt ErrContext) = setErrContext True

666+process h fn (SetOpt ErrContext) = setErrContext True

583−process fn (UnsetOpt ErrContext) = setErrContext False

667+process h fn (UnsetOpt ErrContext) = setErrContext False

584−process fn (SetOpt ShowImpl) = setImpShow True

668+process h fn (SetOpt ShowImpl) = setImpShow True

585−process fn (UnsetOpt ShowImpl) = setImpShow False

669+process h fn (UnsetOpt ShowImpl) = setImpShow False

586−

670+

587−process fn (SetOpt _) = iPrintError "Not a valid option"

671+process h fn (SetOpt _) = iPrintError "Not a valid option"

588−process fn (UnsetOpt _) = iPrintError "Not a valid option"

672+process h fn (UnsetOpt _) = iPrintError "Not a valid option"

589−process fn (SetColour ty c) = setColour ty c

673+process h fn (SetColour ty c) = setColour ty c

590−process fn ColourOn = do ist <- getIState

674+process h fn ColourOn

675+ = do ist <- getIState

591 putIState $ ist { idris_colourRepl = True }

676 putIState $ ist { idris_colourRepl = True }

592−process fn ColourOff = do ist <- getIState

677+process h fn ColourOff

678+ = do ist <- getIState

593 putIState $ ist { idris_colourRepl = False }

679 putIState $ ist { idris_colourRepl = False }

594

680

595−

596classInfo :: ClassInfo -> Idris ()

681classInfo :: ClassInfo -> Idris ()

597classInfo ci = do iputStrLn "Methods:\n"

682classInfo ci = do iputStrLn "Methods:\n"

598 mapM_ dumpMethod (class_methods ci)

683 mapM_ dumpMethod (class_methods ci)

@@ -641,6 +726,7 @@ parseArgs :: [String] -> [Opt]

641parseArgs [] = []

726parseArgs [] = []

642parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

727parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

643parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)

728parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)

729+parseArgs ("--client":ns) = [Client (showSep " " ns)]

644parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

730parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

645parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

731parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

646parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

732parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

@@ -709,8 +795,8 @@ idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit

709 Right ist -> return ()

795 Right ist -> return ()

710

796

711

797

712−loadInputs :: [FilePath] -> Idris ()

798+loadInputs :: Handle -> [FilePath] -> Idris ()

713−loadInputs inputs

799+loadInputs h inputs

714 = do ist <- getIState

800 = do ist <- getIState

715 -- if we're in --check and not outputting anything, don't bother

801 -- if we're in --check and not outputting anything, don't bother

716 -- loading, as it gets really slow if there's lots of modules in

802 -- loading, as it gets really slow if there's lots of modules in

@@ -764,7 +850,7 @@ loadInputs inputs

764 where -- load all files, stop if any fail

850 where -- load all files, stop if any fail

765 tryLoad :: [IFileType] -> Idris ()

851 tryLoad :: [IFileType] -> Idris ()

766 tryLoad [] = return ()

852 tryLoad [] = return ()

767− tryLoad (f : fs) = do loadFromIFile f

853+ tryLoad (f : fs) = do loadFromIFile h f

768 inew <- getIState

854 inew <- getIState

769 case errLine inew of

855 case errLine inew of

770 Nothing -> tryLoad fs

856 Nothing -> tryLoad fs

@@ -837,19 +923,19 @@ idrisMain opts =

837 addPkgDir "base"

923 addPkgDir "base"

838 mapM_ addPkgDir pkgdirs

924 mapM_ addPkgDir pkgdirs

839 elabPrims

925 elabPrims

840− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

926+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

841 return ()

927 return ()

842 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner

928 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner

843 ist <- getIState

929 ist <- getIState

844

930

845− loadInputs inputs

931+ loadInputs stdout inputs

846

932

847 runIO $ hSetBuffering stdout LineBuffering

933 runIO $ hSetBuffering stdout LineBuffering

848

934

849 ok <- noErrors

935 ok <- noErrors

850 when ok $ case output of

936 when ok $ case output of

851 [] -> return ()

937 [] -> return ()

852− (o:_) -> process "" (Compile cgn o)

938+ (o:_) -> process stdout "" (Compile cgn o)

853 case script of

939 case script of

854 Nothing -> return ()

940 Nothing -> return ()

855 Just expr -> execScript expr

941 Just expr -> execScript expr

@@ -857,7 +943,9 @@ idrisMain opts =

857 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

943 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

858

944

859 when runrepl $ initScript

945 when runrepl $ initScript

946+ stvar <- runIO $ newMVar ist

947+ when runrepl $ startServer ist stvar inputs

860− when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs

948+ when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist stvar inputs

861 when (idesl) $ ideslaveStart ist inputs

949 when (idesl) $ ideslaveStart ist inputs

862 ok <- noErrors

950 ok <- noErrors

863 when (not ok) $ runIO (exitWith (ExitFailure 1))

951 when (not ok) $ runIO (exitWith (ExitFailure 1))

@@ -925,7 +1013,7 @@ initScript = do script <- getInitScript

925 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

1013 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

926 Success Proofs -> proofs i

1014 Success Proofs -> proofs i

927 Success Quit -> iPrintError "Init scripts cannot quit Idris"

1015 Success Quit -> iPrintError "Init scripts cannot quit Idris"

928− Success cmd -> process [] cmd

1016+ Success cmd -> process stdout [] cmd

929

1017

930getFile :: Opt -> Maybe String

1018getFile :: Opt -> Maybe String

931getFile (Filename str) = Just str

1019getFile (Filename str) = Just str

src/Idris/REPLParser.hs+3−2

@@ -71,8 +71,9 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

71 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

72 <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

73 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

74+ upd <- option False (do P.lchar '!'; return True)

74− l <- P.natural; n <- P.name;

75+ l <- P.natural; n <- P.name;

75− return (CaseSplitAt (fromInteger l) n))

76+ return (CaseSplitAt upd (fromInteger l) n))

76 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 n <- P.name;

78 n <- P.name;

78 t <- P.fullExpr defaultSyntax;

79 t <- P.fullExpr defaultSyntax;

src/Main.hs+3

@@ -46,6 +46,9 @@ main = do xs <- getArgs

46 Right _ -> return ()

48runIdris :: [Opt] -> Idris ()

49+runIdris [Client c] = do setVerbose False

50+ setQuiet True

51+ runIO $ runClient c

49runIdris opts = do

52runIdris opts = do

50 when (Ver `elem` opts) $ runIO showver

53 when (Ver `elem` opts) $ runIO showver

51 when (Usage `elem` opts) $ runIO usage

54 when (Usage `elem` opts) $ runIO usage