d947282 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1452 from hannesm/ideslave-socket

Ideslave socket

commitd947282dc207f7a9c12f095cf77955e8e8116c52 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 4 Aug 2014, 21:11 (12 years ago) parent2418336 159a99c

14 files changed+483−437

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+10−14 src/Idris/AbsSyntaxTree.hs+6−4 src/Idris/CmdOptions.hs+1 src/Idris/Error.hs+2−3 src/Idris/IdeSlave.hs+20−10 src/Idris/Interactive.hs+27−27 src/Idris/Output.hs+60−63 src/Idris/ParseHelpers.hs+2−2 src/Idris/Parser.hs+24−24 src/Idris/Prover.hs+46−45 src/Idris/REPL.hs+263−234 src/Idris/TypeSearch.hs+6−8 src/Pkg/Package.hs+1−1 src/Util/Net.hs+15−2

src/Idris/AbsSyntax.hs+10−14

@@ -537,7 +537,7 @@ type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "

537537isetPrompt :: String -> Idris ()

538538isetPrompt p = do i <- getIState

539539 case idris_outputmode i of

540− IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

540+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

541541

542542-- | Tell clients how much was parsed and loaded

543543isetLoadedRegion :: Idris ()

@@ -546,8 +546,8 @@ isetLoadedRegion = do i <- getIState

546546 case span of

547547 Just fc ->

548548 case idris_outputmode i of

549− IdeSlave n ->

550− runIO . putStrLn $

549+ IdeSlave n h ->

550+ runIO . hPutStrLn h $

551551 convSExp "set-loaded-region" fc n

552552 Nothing -> return ()

553553

@@ -662,10 +662,10 @@ outputTy :: Idris OutputType

662662outputTy = do i <- getIState

663663 return $ opt_outputTy $ idris_options i

664664

665−setIdeSlave :: Bool -> Idris ()

666−setIdeSlave True = do i <- getIState

667− putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }

668−setIdeSlave False = return ()

665+setIdeSlave :: Bool -> Handle -> Idris ()

666+setIdeSlave True h = do i <- getIState

667+ putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }

668+setIdeSlave False _ = return ()

669669

670670setTargetTriple :: String -> Idris ()

671671setTargetTriple t = do i <- getIState

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

761761setColourise b = do i <- getIState

762762 putIState $ i { idris_colourRepl = b }

763763

764−setOutH :: Handle -> Idris ()

765−setOutH h = do i <- getIState

766− putIState $ i { idris_outh = h }

767−

768764impShow :: Idris Bool

769765impShow = do i <- getIState

770766 return (opt_showimp (idris_options i))

@@ -793,10 +789,10 @@ logLvl l str = do i <- getIState

793789 let lvl = opt_logLevel (idris_options i)

794790 when (lvl >= l) $

795791 case idris_outputmode i of

796− RawOutput -> do runIO $ putStrLn str

797− IdeSlave n ->

792+ RawOutput h -> do runIO $ hPutStrLn h str

793+ IdeSlave n h ->

798794 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]

799− runIO $ putStrLn $ convSExp "log" good n

795+ runIO . hPutStrLn h $ convSExp "log" good n

800796

801797cmdOptType :: Opt -> Idris Bool

802798cmdOptType x = do i <- getIState

src/Idris/AbsSyntaxTree.hs+6−4

@@ -127,7 +127,9 @@ ppOptionIst = ppOption . idris_options

127127data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

128128

129129-- | The output mode in use

130−data OutputMode = RawOutput | IdeSlave Integer deriving Show

130+data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

131+ | IdeSlave Integer Handle -- ^ Send IDE output for some request ID to the handle

132+ deriving Show

131133

132134-- | How wide is the console?

133135data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

@@ -192,7 +194,6 @@ data IState = IState {

192194 idris_outputmode :: OutputMode,

193195 idris_colourRepl :: Bool,

194196 idris_colourTheme :: ColourTheme,

195− idris_outh :: Handle,

196197 idris_errorhandlers :: [Name], -- ^ Global error handlers

197198 idris_nameIdx :: (Int, Ctxt (Int, Name)),

198199 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

@@ -277,8 +278,8 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

277278 emptyContext emptyContext emptyContext emptyContext

278279 emptyContext emptyContext

279280 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

280− [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

281− True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

281+ [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

282+ (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

282283 AutomaticWidth S.empty Nothing Nothing

283284

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

@@ -358,6 +359,7 @@ data Opt = Filename String

358359 | NoBanner

359360 | ColourREPL Bool

360361 | Ideslave

362+ | IdeslaveSocket

361363 | ShowLibs

362364 | ShowLibdir

363365 | ShowIncs

src/Idris/CmdOptions.hs+1

@@ -71,6 +71,7 @@ parseFlags = many $

7171 flag' NoBanner (long "nobanner" <> help "Suppress the banner")

7272 <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

7373 <|> flag' Ideslave (long "ideslave")

74+ <|> flag' IdeslaveSocket (long "ideslave-socket")

7475 <|> (Client <$> strOption (long "client"))

7576 <|> (OLogging <$> option (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

7677 <|> flag' NoBasePkgs (long "nobasepkgs")

src/Idris/Error.hs+2−3

@@ -42,12 +42,11 @@ idrisCatch = catchError

4242

4343setAndReport :: Err -> Idris ()

4444setAndReport e = do ist <- getIState

45− let h = idris_outh ist

4645 case (unwrap e) of

4746 At fc e -> do setErrSpan fc

48− ihWarn h fc $ pprintErr ist e

47+ iWarn fc $ pprintErr ist e

4948 _ -> do setErrSpan (getErrSpan e)

50− ihWarn h emptyFC $ pprintErr ist e

49+ iWarn emptyFC $ pprintErr ist e

5150 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor

5251 unwrap e = e

5352

src/Idris/IdeSlave.hs+20−10

@@ -1,6 +1,6 @@

11{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

3−module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..)) where

3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where

55import Text.Printf

66import Numeric

@@ -12,12 +12,24 @@ import qualified Data.ByteString.UTF8 as UTF8

1212-- import qualified Data.Text as T

1313import Text.Trifecta hiding (Err)

1414import Text.Trifecta.Delta

15+import System.IO

1516

1617import Idris.Core.TT

1718import Idris.Core.Binary

1819

1920import Control.Applicative hiding (Const)

2021

22+getNChar :: Handle -> Int -> String -> IO (String)

23+getNChar _ 0 s = return (reverse s)

24+getNChar h n s = do c <- hGetChar h

25+ getNChar h (n - 1) (c : s)

26+

27+getLen :: Handle -> IO (Either Err Int)

28+getLen h = do s <- getNChar h 6 ""

29+ case readHex s of

30+ ((num, ""):_) -> return $ Right num

31+ _ -> return $ Left . Msg $ "Couldn't read length " ++ s

32+

2133data SExp = SexpList [SExp]

2234 | StringAtom String

2335 | BoolAtom Bool

@@ -247,19 +259,14 @@ sexpToCommand _

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

248260parseMessage x = case receiveString x of

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

262+ Right x -> Left . Msg $ "Invalid message " ++ show x

250263 Left err -> Left err

251264

252265receiveString :: String -> Either Err SExp

253266receiveString x =

254− case readHex (take 6 x) of

255− ((num, ""):_) ->

256− let msg = drop 6 x in

257− if (length msg) /= (num - 1)

258− then Left . Msg $ "bad input length"

259− else (case parseSExp msg of

260− Failure _ -> Left . Msg $ "parse failure"

261− Success r -> Right r)

262− _ -> Left . Msg $ "readHex failed"

267+ case parseSExp x of

268+ Failure _ -> Left . Msg $ "parse failure"

269+ Success r -> Right r

263270

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

265272convSExp pre s id =

@@ -269,3 +276,6 @@ convSExp pre s id =

269276

270277getHexLength :: String -> String

271278getHexLength s = printf "%06x" (1 + (length s))

279+

280+ideSlaveEpoch :: Int

281+ideSlaveEpoch = 1

src/Idris/Interactive.hs+27−27

@@ -31,8 +31,8 @@ import Data.Maybe (fromMaybe)

3131

3232import Debug.Trace

3333

34−caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

35−caseSplitAt h fn updatefile l n

34+caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

35+caseSplitAt fn updatefile l n

3636 = do src <- runIO $ readFile fn

3737 res <- splitOnLine l n fn

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

@@ -43,11 +43,11 @@ caseSplitAt h fn updatefile l n

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

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

4545 runIO $ copyFile fb fn

46− else -- do ihputStrLn h (show res)

47− ihPrintResult h new

46+ else -- do iputStrLn (show res)

47+ iPrintResult new

4848

49−addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

50−addClauseFrom h fn updatefile l n

49+addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

50+addClauseFrom fn updatefile l n

5151 = do src <- runIO $ readFile fn

5252 let (before, tyline : later) = splitAt (l-1) (lines src)

5353 let indent = getIndent 0 (show n) tyline

@@ -61,15 +61,15 @@ addClauseFrom h fn updatefile l n

6161 cl ++ "\n" ++

6262 unlines rest)

6363 runIO $ copyFile fb fn

64− else ihPrintResult h cl

64+ else iPrintResult cl

6565 where

6666 getIndent i n [] = 0

6767 getIndent i n xs | take 9 xs == "instance " = i

6868 getIndent i n xs | take (length n) xs == n = i

6969 getIndent i n (x : xs) = getIndent (i + 1) n xs

7070

71−addProofClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

72−addProofClauseFrom h fn updatefile l n

71+addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

72+addProofClauseFrom fn updatefile l n

7373 = do src <- runIO $ readFile fn

7474 let (before, tyline : later) = splitAt (l-1) (lines src)

7575 let indent = getIndent 0 (show n) tyline

@@ -83,14 +83,14 @@ addProofClauseFrom h fn updatefile l n

8383 cl ++ "\n" ++

8484 unlines rest)

8585 runIO $ copyFile fb fn

86− else ihPrintResult h cl

86+ else iPrintResult cl

8787 where

8888 getIndent i n [] = 0

8989 getIndent i n xs | take (length n) xs == n = i

9090 getIndent i n (x : xs) = getIndent (i + 1) n xs

9191

92−addMissing :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

93−addMissing h fn updatefile l n

92+addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

93+addMissing fn updatefile l n

9494 = do src <- runIO $ readFile fn

9595 let (before, tyline : later) = splitAt (l-1) (lines src)

9696 let indent = getIndent 0 (show n) tyline

@@ -108,7 +108,7 @@ addMissing h fn updatefile l n

108108 runIO $ writeFile fb (unlines (before ++ nonblank)

109109 ++ extras ++ unlines rest)

110110 runIO $ copyFile fb fn

111− else ihPrintResult h extras

111+ else iPrintResult extras

112112 where showPat = show . stripNS

113113 stripNS tm = mapPT dens tm where

114114 dens (PRef fc n) = PRef fc (nsroot n)

@@ -135,8 +135,8 @@ addMissing h fn updatefile l n

135135 getIndent i n (x : xs) = getIndent (i + 1) n xs

136136

137137

138−makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

139−makeWith h fn updatefile l n

138+makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

139+makeWith fn updatefile l n

140140 = do src <- runIO $ readFile fn

141141 let (before, tyline : later) = splitAt (l-1) (lines src)

142142 let ind = getIndent tyline

@@ -151,15 +151,15 @@ makeWith h fn updatefile l n

151151 ++ with ++ "\n" ++

152152 unlines rest)

153153 runIO $ copyFile fb fn

154− else ihPrintResult h with

154+ else iPrintResult with

155155 where getIndent s = length (takeWhile isSpace s)

156156

157157

158−doProofSearch :: Handle -> FilePath -> Bool -> Bool ->

158+doProofSearch :: FilePath -> Bool -> Bool ->

159159 Int -> Name -> [Name] -> Maybe Int -> Idris ()

160−doProofSearch h fn updatefile rec l n hints Nothing

161− = doProofSearch h fn updatefile rec l n hints (Just 10)

162−doProofSearch h fn updatefile rec l n hints (Just depth)

160+doProofSearch fn updatefile rec l n hints Nothing

161+ = doProofSearch fn updatefile rec l n hints (Just 10)

162+doProofSearch fn updatefile rec l n hints (Just depth)

163163 = do src <- runIO $ readFile fn

164164 let (before, tyline : later) = splitAt (l-1) (lines src)

165165 ctxt <- getContext

@@ -192,7 +192,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

192192 updateMeta False tyline (show n) newmv ++ "\n"

193193 ++ unlines later)

194194 runIO $ copyFile fb fn

195− else ihPrintResult h newmv

195+ else iPrintResult newmv

196196 where dropCtxt 0 sc = sc

197197 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

198198 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

@@ -235,8 +235,8 @@ addBracket True new | any isSpace new = '(' : new ++ ")"

235235 | otherwise = new

236236

237237

238−makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

239−makeLemma h fn updatefile l n

238+makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()

239+makeLemma fn updatefile l n

240240 = do src <- runIO $ readFile fn

241241 let (before, tyline : later) = splitAt (l-1) (lines src)

242242

@@ -266,8 +266,8 @@ makeLemma h fn updatefile l n

266266 runIO $ writeFile fb (addLem before tyline lem lem_app later)

267267 runIO $ copyFile fb fn

268268 else case idris_outputmode i of

269− RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app

270− IdeSlave n ->

269+ RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app

270+ IdeSlave n h ->

271271 let good = SexpList [SymbolAtom "ok",

272272 SexpList [SymbolAtom "metavariable-lemma",

273273 SexpList [SymbolAtom "replace-metavariable",

@@ -284,8 +284,8 @@ makeLemma h fn updatefile l n

284284 runIO $ writeFile fb (addProv before tyline lem_app later)

285285 runIO $ copyFile fb fn

286286 else case idris_outputmode i of

287− RawOutput -> ihPrintResult h $ lem_app

288− IdeSlave n ->

287+ RawOutput _ -> iPrintResult $ lem_app

288+ IdeSlave n h ->

289289 let good = SexpList [SymbolAtom "ok",

290290 SexpList [SymbolAtom "provisional-definition-lemma",

291291 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+60−63

@@ -24,27 +24,28 @@ pshow ist err = displayDecorated (consoleDecorate ist) .

2424 renderPretty 1.0 80 .

2525 fmap (fancifyAnnots ist) $ pprintErr ist err

2626

27−ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

28−ihWarn h fc err = do i <- getIState

29− case idris_outputmode i of

30− RawOutput ->

31− do err' <- iRender . fmap (fancifyAnnots i) $

32− if fc_fname fc /= ""

33− then text (show fc) <> colon <//> err

34− else err

35− runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

36− IdeSlave n ->

37− do err' <- iRender . fmap (fancifyAnnots i) $ err

38− let (str, spans) = displaySpans err'

39− runIO . hPutStrLn h $

40− convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

27+iWarn :: FC -> Doc OutputAnnotation -> Idris ()

28+iWarn fc err =

29+ do i <- getIState

30+ case idris_outputmode i of

31+ RawOutput h ->

32+ do err' <- iRender . fmap (fancifyAnnots i) $

33+ if fc_fname fc /= ""

34+ then text (show fc) <> colon <//> err

35+ else err

36+ runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

37+ IdeSlave n h ->

38+ do err' <- iRender . fmap (fancifyAnnots i) $ err

39+ let (str, spans) = displaySpans err'

40+ runIO . hPutStrLn h $

41+ convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

4142

4243iRender :: Doc a -> Idris (SimpleDoc a)

4344iRender d = do w <- getWidth

4445 ist <- getIState

4546 let ideSlave = case idris_outputmode ist of

46− IdeSlave _ -> True

47− _ -> False

47+ IdeSlave _ _ -> True

48+ _ -> False

4849 case w of

4950 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

5051 ColsWide n -> return $

@@ -63,37 +64,37 @@ consoleDisplayAnnotated h output = do ist <- getIState

6364 displayDecorated (consoleDecorate ist) $

6465 rendered

6566

66−ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

67−ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)

67+iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

68+iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

6869

6970-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

70−ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

71−ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

72−ihPrintFunTypes h bnd n overloads = do ist <- getIState

73− let ppo = ppOptionIst ist

74− let infixes = idris_infixes ist

75− let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

76− ihRenderResult h output

71+iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

72+iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n

73+iPrintFunTypes bnd n overloads = do ist <- getIState

74+ let ppo = ppOptionIst ist

75+ let infixes = idris_infixes ist

76+ let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

77+ iRenderResult output

7778 where fullName n = prettyName True True bnd n

7879 ppOverload ppo infixes n tm =

7980 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

8081

81−ihRenderOutput :: Handle -> Doc OutputAnnotation -> Idris ()

82−ihRenderOutput h doc =

82+iRenderOutput :: Doc OutputAnnotation -> Idris ()

83+iRenderOutput doc =

8384 do i <- getIState

8485 case idris_outputmode i of

85− RawOutput -> do out <- iRender doc

86− runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

87− IdeSlave n ->

86+ RawOutput h -> do out <- iRender doc

87+ runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

88+ IdeSlave n h ->

8889 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

8990 let out = [toSExp str, toSExp spans]

90− runIO . putStrLn $ convSExp "write-decorated" out n

91+ runIO . hPutStrLn h $ convSExp "write-decorated" out n

9192

92−ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

93−ihRenderResult h d = do ist <- getIState

94− case idris_outputmode ist of

95− RawOutput -> consoleDisplayAnnotated h d

96− IdeSlave n -> ideSlaveReturnAnnotated n h d

93+iRenderResult :: Doc OutputAnnotation -> Idris ()

94+iRenderResult d = do ist <- getIState

95+ case idris_outputmode ist of

96+ RawOutput h -> consoleDisplayAnnotated h d

97+ IdeSlave n h -> ideSlaveReturnAnnotated n h d

9798

9899ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

99100ideSlaveReturnWithStatus status n h out = do

@@ -111,56 +112,52 @@ ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

111112ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

112113

113114-- | Show an error with semantic highlighting

114−ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

115−ihRenderError h e = do ist <- getIState

116− case idris_outputmode ist of

117− RawOutput -> consoleDisplayAnnotated h e

118− IdeSlave n -> ideSlaveReturnWithStatus "error" n h e

119−

120−ihPrintWithStatus :: String -> Handle -> String -> Idris ()

121−ihPrintWithStatus status h s = do

115+iRenderError :: Doc OutputAnnotation -> Idris ()

116+iRenderError e = do ist <- getIState

117+ case idris_outputmode ist of

118+ RawOutput h -> consoleDisplayAnnotated h e

119+ IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e

120+

121+iPrintWithStatus :: String -> String -> Idris ()

122+iPrintWithStatus status s = do

122123 i <- getIState

123124 case idris_outputmode i of

124− RawOutput -> case s of

125+ RawOutput h -> case s of

125126 "" -> return ()

126127 s -> runIO $ hPutStrLn h s

127− IdeSlave n ->

128+ IdeSlave n h ->

128129 let good = SexpList [SymbolAtom status, toSExp s] in

129130 runIO $ hPutStrLn h $ convSExp "return" good n

130131

131132

132−ihPrintResult :: Handle -> String -> Idris ()

133−ihPrintResult = ihPrintWithStatus "ok"

133+iPrintResult :: String -> Idris ()

134+iPrintResult = iPrintWithStatus "ok"

134135

135−ihPrintError :: Handle -> String -> Idris ()

136−ihPrintError = ihPrintWithStatus "error"

136+iPrintError :: String -> Idris ()

137+iPrintError = iPrintWithStatus "error"

137138

138−ihputStrLn :: Handle -> String -> Idris ()

139−ihputStrLn h s = do i <- getIState

140− case idris_outputmode i of

141− RawOutput -> runIO $ hPutStrLn h s

142− IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

139+iputStrLn :: String -> Idris ()

140+iputStrLn s = do i <- getIState

141+ case idris_outputmode i of

142+ RawOutput h -> runIO $ hPutStrLn h s

143+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

143144

144−iputStrLn = ihputStrLn stdout

145−iPrintError = ihPrintError stdout

146−iPrintResult = ihPrintResult stdout

147−iWarn = ihWarn stdout

148145

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

150147ideslavePutSExp cmd info = do i <- getIState

151148 case idris_outputmode i of

152− IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

149+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n

153150 _ -> return ()

154151

155152-- TODO: send structured output similar to the metavariable list

156153iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

157154iputGoal g = do i <- getIState

158155 case idris_outputmode i of

159− RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

160− IdeSlave n ->

156+ RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)

157+ IdeSlave n h ->

161158 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g

162159 goal = [toSExp str, toSExp spans]

163− in runIO . putStrLn $ convSExp "write-goal" goal n

160+ in runIO . hPutStrLn h $ convSExp "write-goal" goal n

164161

165162-- | Warn about totality problems without failing to compile

166163warnTotality :: Idris ()

src/Idris/ParseHelpers.hs+2−2

@@ -17,7 +17,7 @@ import Idris.Core.TT

1717import Idris.Core.Evaluate

1818import Idris.Delaborate (pprintErr)

1919import Idris.Docstrings

20−import Idris.Output (ihWarn)

20+import Idris.Output (iWarn)

2121

2222import qualified Util.Pretty as Pretty (text)

2323

@@ -79,7 +79,7 @@ clearParserWarnings = do ist <- getIState

7979

8080reportParserWarnings :: Idris ()

8181reportParserWarnings = do ist <- getIState

82− mapM_ (uncurry $ ihWarn (idris_outh ist))

82+ mapM_ (uncurry iWarn)

8383 (map (\ (fc, err) -> (fc, pprintErr ist err)) .

8484 reverse .

8585 nub $

src/Idris/Parser.hs+24−24

@@ -1159,8 +1159,8 @@ parseProg syn fname input mrk

11591159 let (fc, msg) = findFC doc

11601160 i <- getIState

11611161 case idris_outputmode i of

1162− RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)

1163− IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1162+ RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1163+ IdeSlave n h -> iWarn fc (P.text msg)

11641164 putIState (i { errSpan = Just fc })

11651165 return []

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

@@ -1176,17 +1176,17 @@ parseProg syn fname input mrk

11761176 return (ds, i')

11771177

11781178{- | Load idris module and show error if something wrong happens -}

1179−loadModule :: Handle -> FilePath -> Idris String

1180−loadModule outh f

1181− = idrisCatch (loadModule' outh f)

1179+loadModule :: FilePath -> Idris String

1180+loadModule f

1181+ = idrisCatch (loadModule' f)

11821182 (\e -> do setErrSpan (getErrSpan e)

11831183 ist <- getIState

1184− ihWarn outh (getErrSpan e) $ pprintErr ist e

1184+ iWarn (getErrSpan e) $ pprintErr ist e

11851185 return "")

11861186

11871187{- | Load idris module -}

1188−loadModule' :: Handle -> FilePath -> Idris String

1189−loadModule' outh f

1188+loadModule' :: FilePath -> Idris String

1189+loadModule' f

11901190 = do i <- getIState

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

11921192 ibcsd <- valIBCSubDir i

@@ -1196,21 +1196,21 @@ loadModule' outh f

11961196 then iLOG $ "Already read " ++ file

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

11981198 case fp of

1199− IDR fn -> loadSource outh False fn Nothing

1200− LIDR fn -> loadSource outh True fn Nothing

1199+ IDR fn -> loadSource False fn Nothing

1200+ LIDR fn -> loadSource True fn Nothing

12011201 IBC fn src ->

12021202 idrisCatch (loadIBC fn)

12031203 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c

12041204 case src of

1205− IDR sfn -> loadSource outh False sfn Nothing

1206− LIDR sfn -> loadSource outh True sfn Nothing)

1205+ IDR sfn -> loadSource False sfn Nothing

1206+ LIDR sfn -> loadSource True sfn Nothing)

12071207 let (dir, fh) = splitFileName file

12081208 return (dropExtension fh)

12091209

12101210

12111211{- | Load idris code from file -}

1212−loadFromIFile :: Handle -> IFileType -> Maybe Int -> Idris ()

1213−loadFromIFile h i@(IBC fn src) maxline

1212+loadFromIFile :: IFileType -> Maybe Int -> Idris ()

1213+loadFromIFile i@(IBC fn src) maxline

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

12151215 idrisCatch (loadIBC fn)

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

@@ -1219,22 +1219,22 @@ loadFromIFile h i@(IBC fn src) maxline

12191219 getSrcFile (LIDR fn) = fn

12201220 getSrcFile (IBC f src) = getSrcFile src

12211221

1222−loadFromIFile h (IDR fn) maxline = loadSource' h False fn maxline

1223−loadFromIFile h (LIDR fn) maxline = loadSource' h True fn maxline

1222+loadFromIFile (IDR fn) maxline = loadSource' False fn maxline

1223+loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline

12241224

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

1226−loadSource' :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()

1227−loadSource' h lidr r maxline

1228− = idrisCatch (loadSource h lidr r maxline)

1226+loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()

1227+loadSource' lidr r maxline

1228+ = idrisCatch (loadSource lidr r maxline)

12291229 (\e -> do setErrSpan (getErrSpan e)

12301230 ist <- getIState

12311231 case e of

1232− At f e' -> ihWarn h f (pprintErr ist e')

1233− _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

1232+ At f e' -> iWarn f (pprintErr ist e')

1233+ _ -> iWarn (getErrSpan e) (pprintErr ist e))

12341234

12351235{- | Load Idris source code-}

1236−loadSource :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()

1237−loadSource h lidr f toline

1236+loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

1237+loadSource lidr f toline

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

12391239 i <- getIState

12401240 let def_total = default_total i

@@ -1278,7 +1278,7 @@ loadSource h lidr f toline

12781278 logLvl 3 (show (idris_infixes i))

12791279 -- Now add all the declarations to the context

12801280 v <- verbose

1281− when v $ ihputStrLn h $ "Type checking " ++ f

1281+ when v $ iputStrLn $ "Type checking " ++ f

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

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

12841284 -- mutual block on its own

src/Idris/Prover.hs+46−45

@@ -19,12 +19,13 @@ import Idris.Parser hiding (params)

1919import Idris.Error

2020import Idris.DataOpts

2121import Idris.Completion

22−import Idris.IdeSlave

22+import qualified Idris.IdeSlave as IdeSlave

2323import Idris.Output

2424import Idris.TypeSearch (searchByType)

2525

2626import Text.Trifecta.Result(Result(..))

2727

28+import System.IO (Handle, stdin, stdout, hPutStrLn)

2829import System.Console.Haskeline

2930import System.Console.Haskeline.History

3031import Control.Monad.State.Strict

@@ -70,8 +71,8 @@ prove opt ctxt lit n ty

7071 iLOG $ "Adding " ++ show tm

7172 i <- getIState

7273 case idris_outputmode i of

73− IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

74− _ -> iputStrLn $ showProof lit n prf

74+ IdeSlave _ _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

75+ _ -> iputStrLn $ showProof lit n prf

7576 let proofs = proof_list i

7677 putIState (i { proof_list = (n, prf) : proofs })

7778 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

@@ -93,9 +94,8 @@ prove opt ctxt lit n ty

9394 [([], P Ref n ty, ptm')] ty)

9495 solveDeferred n

9596 case idris_outputmode i of

96− IdeSlave n ->

97− runIO . putStrLn $

98− convSExp "return" (SymbolAtom "ok", "") n

97+ IdeSlave n h ->

98+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n

9999 _ -> return ()

100100

101101elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

@@ -177,23 +177,28 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a

177177lifte st e = do (v, _) <- elabStep st e

178178 return v

179179

180−receiveInput :: ElabState [PDecl] -> Idris (Maybe String)

181−receiveInput e =

180+receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)

181+receiveInput h e =

182182 do i <- getIState

183− l <- runIO $ getLine

184− (sexp, id) <- case parseMessage l of

183+ let inh = if h == stdout then stdin else h

184+ len' <- runIO $ IdeSlave.getLen inh

185+ len <- case len' of

186+ Left err -> ierror err

187+ Right n -> return n

188+ l <- runIO $ IdeSlave.getNChar inh len ""

189+ (sexp, id) <- case IdeSlave.parseMessage l of

185190 Left err -> ierror err

186191 Right (sexp, id) -> return (sexp, id)

187− putIState $ i { idris_outputmode = (IdeSlave id) }

188− case sexpToCommand sexp of

189− Just (REPLCompletions prefix) ->

192+ putIState $ i { idris_outputmode = (IdeSlave id h) }

193+ case IdeSlave.sexpToCommand sexp of

194+ Just (IdeSlave.REPLCompletions prefix) ->

190195 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

191− let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

196+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

192197 ideslavePutSExp "return" good

193− receiveInput e

194− Just (Interpret cmd) -> return (Just cmd)

195− Just (TypeOf str) -> return (Just (":t " ++ str))

196− Just (DocsFor str) -> return (Just (":doc " ++ str))

198+ receiveInput h e

199+ Just (IdeSlave.Interpret cmd) -> return (Just cmd)

200+ Just (IdeSlave.TypeOf str) -> return (Just (":t " ++ str))

201+ Just (IdeSlave.DocsFor str) -> return (Just (":doc " ++ str))

197202 _ -> return Nothing

198203

199204ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

@@ -203,17 +208,18 @@ ploop fn d prompt prf e h

203208 when d $ dumpState i (proof e)

204209 (x, h') <-

205210 case idris_outputmode i of

206− RawOutput -> runInputT (proverSettings e) $

207− -- Manually track the history so that we can use the proof state

208− do _ <- case h of

209− Just history -> putHistory history

210− Nothing -> return ()

211− l <- getInputLine (prompt ++ "> ")

212− h' <- getHistory

213− return (l, Just h')

214− IdeSlave n ->

211+ RawOutput _ ->

212+ runInputT (proverSettings e) $

213+ -- Manually track the history so that we can use the proof state

214+ do case h of

215+ Just history -> putHistory history

216+ Nothing -> return ()

217+ l <- getInputLine (prompt ++ "> ")

218+ h' <- getHistory

219+ return (l, Just h')

220+ IdeSlave _ handle ->

215221 do isetPrompt prompt

216− i <- receiveInput e

222+ i <- receiveInput handle e

217223 return (i, h)

218224 (cmd, step) <- case x of

219225 Nothing -> do iPrintError ""; ifail "Abandoned"

@@ -245,7 +251,8 @@ ploop fn d prompt prf e h

245251 (\err -> return (False, e, False, prf, Left err))

246252 ideslavePutSExp "write-proof-state" (prf', length prf')

247253 case res of

248− Left err -> do iPrintError (pshow i err)

254+ Left err -> do ist <- getIState

255+ iRenderError $ pprintErr ist err

249256 ploop fn d prompt prf' st h'

250257 Right ok ->

251258 if done then do (tm, _) <- elabStep st get_term

@@ -258,8 +265,7 @@ ploop fn d prompt prf e h

258265 ist <- getIState

259266 imp <- impShow

260267 idrisCatch (do

261− let h = idris_outh ist

262− OK env = envAtFocus (proof e)

268+ let OK env = envAtFocus (proof e)

263269 ctxt' = envCtxt env ctxt

264270 bnd = map (\x -> (fst x, False)) env

265271 ist' = ist { tt_ctxt = ctxt' }

@@ -267,8 +273,8 @@ ploop fn d prompt prf e h

267273 -- Unlike the REPL, metavars have no special treatment, to

268274 -- make it easier to see how to prove with them.

269275 let action = case lookupNames n ctxt' of

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

271− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

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

277+ ts -> iPrintFunTypes bnd n (map (\n -> (n, delabTy ist' n)) ts)

272278 putIState ist

273279 return (False, e, False, prf, Right action))

274280 (\err -> do putIState ist ; ierror err)

@@ -283,14 +289,13 @@ ploop fn d prompt prf e h

283289 (tm, ty) <- elabVal recinfo ERHS t

284290 let ppo = ppOptionIst ist

285291 ty' = normaliseC ctxt [] ty

286− h = idris_outh ist

287292 infixes = idris_infixes ist

288293 action = case tm of

289294 TType _ ->

290− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

295+ iPrintTermWithType (prettyImp ppo PType) type1Doc

291296 _ -> let bnd = map (\x -> (fst x, False)) env in

292− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

293− (pprintPTerm ppo bnd [] infixes (delab ist ty))

297+ iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))

298+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

294299 putIState ist

295300 return (False, e, False, prf, Right action))

296301 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -311,25 +316,21 @@ ploop fn d prompt prf e h

311316 infixes = idris_infixes ist

312317 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

313318 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

314− action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

319+ action = iPrintTermWithType tmDoc tyDoc

315320 putIState ist

316321 return (False, e, False, prf, Right action))

317322 (\err -> do putIState ist ; ierror err)

318323 docStr :: Either Name Const -> Idris (Bool, ElabState [PDecl], Bool, [String], Either Err (Idris ()))

319324 docStr (Left n) = do ist <- getIState

320− let h = idris_outh ist

321325 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

322326 [] -> return (False, e, False, prf,

323327 Left . Msg $ "No documentation for " ++ show n)

324328 ns -> do toShow <- mapM (showDoc ist) ns

325329 return (False, e, False, prf,

326− Right $ ihRenderResult h (vsep toShow)))

330+ Right $ iRenderResult (vsep toShow)))

327331 (\err -> do putIState ist ; ierror err)

328332 where showDoc ist (n, d) = do doc <- getDocs n

329333 return $ pprintDocs ist doc

330334 docStr (Right c) = do ist <- getIState

331− let h = idris_outh ist

332− return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))

333− search t = do ist <- getIState

334− let h = idris_outh ist

335− return (False, e, False, prf, Right $ searchByType h t)

335+ return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

336+ search t = return (False, e, False, prf, Right $ searchByType t)

src/Idris/REPL.hs+263−234

@@ -42,7 +42,7 @@ import Idris.Elab.Value

4242import Version_idris (gitHash)

4343import Util.System

4444import Util.DynamicLinker

45−import Util.Net (listenOnLocalhost)

45+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

4646import Util.Pretty hiding ((</>))

4747

4848import Idris.Core.Evaluate

@@ -91,6 +91,8 @@ import Data.Word (Word)

9191import Data.Either (partitionEithers)

9292import Control.DeepSeq

9393

94+import Numeric ( readHex )

95+

9496import Debug.Trace

9597

9698-- | Run the REPL

@@ -149,7 +151,7 @@ startServer orig fn_in = do tid <- runIO $ forkOS serverLoop

149151 -- TODO: option for port number

150152 serverLoop = withSocketsDo $

151153 do sock <- listenOnLocalhost $ PortNumber 4294

152− loop fn orig sock

154+ loop fn orig { idris_colourRepl = False } sock

153155

154156 fn = case fn_in of

155157 (f:_) -> f

@@ -159,7 +161,10 @@ startServer orig fn_in = do tid <- runIO $ forkOS serverLoop

159161 = do (h,_,_) <- accept sock

160162 hSetEncoding h utf8

161163 cmd <- hGetLine h

162− (ist', fn) <- processNetCmd orig ist h fn cmd

164+ let isth = case idris_outputmode ist of

165+ RawOutput _ -> ist {idris_outputmode = RawOutput h}

166+ IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

167+ (ist', fn) <- processNetCmd orig isth h fn cmd

163168 hClose h

164169 loop fn ist' sock

165170

@@ -185,12 +190,18 @@ processNetCmd orig i h fn cmd

185190 setOutH h

186191 setQuiet True

187192 setVerbose False

188− mods <- loadInputs h [f] toline

193+ mods <- loadInputs [f] toline

189194 ist <- getIState

190195 return (ist, f)

191− processNet fn c = do process h fn c

196+ processNet fn c = do process fn c

192197 ist <- getIState

193198 return (ist, fn)

199+ setOutH :: Handle -> Idris ()

200+ setOutH h =

201+ do ist <- getIState

202+ putIState $ case idris_outputmode ist of

203+ RawOutput _ -> ist {idris_outputmode = RawOutput h}

204+ IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

194205

195206-- | Run a command on the server on localhost

196207runClient :: String -> IO ()

@@ -206,55 +217,73 @@ runClient str = withSocketsDo $ do

206217 else do l <- hGetLine h

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

208219

220+initIdeslaveSocket :: IO Handle

221+initIdeslaveSocket = do

222+ (sock, port) <- listenOnLocalhostAnyPort

223+ putStrLn $ show port

224+ (h, _, _) <- accept sock

225+ hSetEncoding h utf8

226+ return h

227+

209228-- | Run the IdeSlave

210−ideslaveStart :: IState -> [FilePath] -> Idris ()

211−ideslaveStart orig mods

212− = do i <- getIState

229+ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()

230+ideslaveStart s orig mods

231+ = do h <- runIO $ if s then initIdeslaveSocket else return stdout

232+ setIdeSlave True h

233+ i <- getIState

213234 case idris_outputmode i of

214− IdeSlave n ->

215− when (mods /= []) (do isetPrompt (mkPrompt mods))

216− ideslave orig mods

217−

218−

219−ideslave :: IState -> [FilePath] -> Idris ()

220−ideslave orig mods

235+ IdeSlave n h ->

236+ do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n

237+ case mods of

238+ a:_ -> runIdeSlaveCommand h n i "" [] (IdeSlave.LoadFile a Nothing)

239+ _ -> return ()

240+ ideslave h orig mods

241+

242+ideslave :: Handle -> IState -> [FilePath] -> Idris ()

243+ideslave h orig mods

221244 = do idrisCatch

222− (do l <- runIO $ getLine

245+ (do let inh = if h == stdout then stdin else h

246+ len' <- runIO $ IdeSlave.getLen inh

247+ len <- case len' of

248+ Left err -> ierror err

249+ Right n -> return n

250+ l <- runIO $ IdeSlave.getNChar inh len ""

223251 (sexp, id) <- case IdeSlave.parseMessage l of

224252 Left err -> ierror err

225253 Right (sexp, id) -> return (sexp, id)

226254 i <- getIState

227− putIState $ i { idris_outputmode = (IdeSlave id) }

255+ putIState $ i { idris_outputmode = (IdeSlave id h) }

228256 idrisCatch -- to report correct id back!

229257 (do let fn = case mods of

230258 (f:_) -> f

231− _ -> ""

259+ _ -> ""

232260 case IdeSlave.sexpToCommand sexp of

233− Just cmd -> runIdeSlaveCommand id orig fn mods cmd

261+ Just cmd -> runIdeSlaveCommand h id orig fn mods cmd

234262 Nothing -> iPrintError "did not understand" )

235263 (\e -> do iPrintError $ show e))

236264 (\e -> do iPrintError $ show e)

237− ideslave orig mods

265+ ideslave h orig mods

238266

239267-- | Run IDESlave commands

240−runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client

268+runIdeSlaveCommand :: Handle -- ^^ The handle for communication

269+ -> Integer -- ^^ The continuation ID for the client

241270 -> IState -- ^^ The original IState

242271 -> FilePath -- ^^ The current open file

243272 -> [FilePath] -- ^^ The currently loaded modules

244273 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

245274 -> Idris ()

246−runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

275+runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

247276 do c <- colourise

248277 i <- getIState

249278 case parseCmd i "(input)" cmd of

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

251280 Success (Prove n') ->

252281 idrisCatch

253− (do process stdout fn (Prove n')

282+ (do process fn (Prove n')

254283 isetPrompt (mkPrompt mods)

255284 case idris_outputmode i of

256− IdeSlave n -> -- signal completion of proof to ide

257− runIO . hPutStrLn stdout $

285+ IdeSlave n h -> -- signal completion of proof to ide

286+ runIO . hPutStrLn h $

258287 IdeSlave.convSExp "return"

259288 (IdeSlave.SymbolAtom "ok", "")

260289 n

@@ -262,26 +291,26 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

262291 (\e -> do ist <- getIState

263292 isetPrompt (mkPrompt mods)

264293 case idris_outputmode i of

265− IdeSlave n ->

266− runIO . hPutStrLn stdout $

294+ IdeSlave n h ->

295+ runIO . hPutStrLn h $

267296 IdeSlave.convSExp "abandon-proof" "Abandoned" n

268297 _ -> return ()

269− ihRenderError stdout $ pprintErr ist e)

298+ iRenderError $ pprintErr ist e)

270299 Success cmd -> idrisCatch

271300 (ideslaveProcess fn cmd)

272− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

273−runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =

301+ (\e -> getIState >>= iRenderError . flip pprintErr e)

302+runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =

274303 do (unused, compls) <- replCompletion (reverse str, "")

275304 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

276305 IdeSlave.toSExp (map replacement compls,

277306 reverse unused)]

278− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

279−runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

307+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id

308+runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

280309 do i <- getIState

281310 clearErr

282311 putIState (orig { idris_options = idris_options i,

283− idris_outputmode = (IdeSlave id) })

284− loadInputs stdout [filename] toline

312+ idris_outputmode = (IdeSlave id h) })

313+ loadInputs [filename] toline

285314 isetPrompt (mkPrompt [filename])

286315 -- Report either success or failure

287316 i <- getIState

@@ -291,45 +320,45 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

291320 (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

292321 IdeSlave.toSExp fc])

293322 (idris_parsedSpan i)

294− in runIO . putStrLn $ IdeSlave.convSExp "return" msg id

323+ in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

295324 Just x -> iPrintError $ "didn't load " ++ filename

296− ideslave orig [filename]

297−runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

325+ ideslave h orig [filename]

326+runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =

298327 case splitName name of

299328 Left err -> iPrintError err

300− Right n -> process stdout "(ideslave)"

329+ Right n -> process "(ideslave)"

301330 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

302331 where splitName :: String -> Either String Name

303332 splitName s = case reverse $ splitOn "." s of

304333 [] -> Left ("Didn't understand name '" ++ s ++ "'")

305334 [n] -> Right $ sUN n

306335 (n:ns) -> Right $ sNS (sUN n) ns

307−runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

336+runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =

308337 case parseConst orig name of

309− Success c -> process stdout "(ideslave)" (DocStr (Right c))

338+ Success c -> process "(ideslave)" (DocStr (Right c))

310339 Failure _ ->

311340 case splitName name of

312341 Left err -> iPrintError err

313− Right n -> process stdout "(ideslave)" (DocStr (Left n))

314−runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

315− process stdout fn (CaseSplitAt False line (sUN name))

316−runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

317− process stdout fn (AddClauseFrom False line (sUN name))

318−runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =

319− process stdout fn (AddProofClauseFrom False line (sUN name))

320−runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

321− process stdout fn (AddMissing False line (sUN name))

322−runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

323− process stdout fn (MakeWith False line (sUN name))

324−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

325− doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth

326−runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

342+ Right n -> process "(ideslave)" (DocStr (Left n))

343+runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =

344+ process fn (CaseSplitAt False line (sUN name))

345+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =

346+ process fn (AddClauseFrom False line (sUN name))

347+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =

348+ process fn (AddProofClauseFrom False line (sUN name))

349+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =

350+ process fn (AddMissing False line (sUN name))

351+runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =

352+ process fn (MakeWith False line (sUN name))

353+runIdeSlaveCommand h id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

354+ doProofSearch fn False r line (sUN name) (map sUN hints) depth

355+runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =

327356 case splitName name of

328357 Left err -> iPrintError err

329− Right n -> process stdout fn (MakeLemma False line n)

330−runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

331− process stdout fn (Apropos a)

332−runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

358+ Right n -> process fn (MakeLemma False line n)

359+runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =

360+ process fn (Apropos a)

361+runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =

333362 do ist <- getIState

334363 let opts = idris_options ist

335364 let impshow = opt_showimp opts

@@ -337,16 +366,16 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

337366 let options = (IdeSlave.SymbolAtom "ok",

338367 [(IdeSlave.SymbolAtom "show-implicits", impshow),

339368 (IdeSlave.SymbolAtom "error-context", errCtxt)])

340− runIO . putStrLn $ IdeSlave.convSExp "return" options id

341−runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

369+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id

370+runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

342371 do setImpShow b

343372 let msg = (IdeSlave.SymbolAtom "ok", b)

344− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

345−runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

373+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

374+runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

346375 do setErrContext b

347376 let msg = (IdeSlave.SymbolAtom "ok", b)

348− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

349−runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

377+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

378+runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

350379 do ist <- getIState

351380 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

352381 let ppo = ppOptionIst ist

@@ -362,7 +391,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

362391 (zip bnds hs),

363392 render ist bnd c pc))

364393 splitMvs

365− runIO . putStrLn $

394+ runIO . hPutStrLn h $

366395 IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id

367396 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

368397 mapSnd f xs = zip (map fst xs) (map (f . snd) xs)

@@ -407,32 +436,32 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

407436 let (out, spans) = render ist bnd t pt in

408437 (show n , out, spans)

409438

410−runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

439+runIdeSlaveCommand h id orig fn mods (IdeSlave.WhoCalls n) =

411440 case splitName n of

412441 Left err -> iPrintError err

413442 Right n -> do calls <- whoCalls n

414443 ist <- getIState

415444 let msg = (IdeSlave.SymbolAtom "ok",

416445 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

417− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

446+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

418447 where pn ist = displaySpans .

419448 renderPretty 0.9 1000 .

420449 fmap (fancifyAnnots ist) .

421450 prettyName True True []

422−runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =

451+runIdeSlaveCommand h id orig fn mods (IdeSlave.CallsWho n) =

423452 case splitName n of

424453 Left err -> iPrintError err

425454 Right n -> do calls <- callsWho n

426455 ist <- getIState

427456 let msg = (IdeSlave.SymbolAtom "ok",

428457 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

429− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

458+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

430459 where pn ist = displaySpans .

431460 renderPretty 0.9 1000 .

432461 fmap (fancifyAnnots ist) .

433462 prettyName True True []

434463

435−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

464+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =

436465 do ctxt <- getContext

437466 ist <- getIState

438467 let tm' = force (normaliseAll ctxt [] tm)

@@ -446,15 +475,15 @@ runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

446475 displaySpans .

447476 renderPretty 0.9 80 .

448477 fmap (fancifyAnnots ist) $ ptm)

449− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

450−runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

451− ideSlaveForceTermImplicits id bnd True tm

452−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

453− ideSlaveForceTermImplicits id bnd False tm

478+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

479+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

480+ ideSlaveForceTermImplicits h id bnd True tm

481+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

482+ ideSlaveForceTermImplicits h id bnd False tm

454483

455484-- | Show a term for IDESlave with the specified implicitness

456−ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

457−ideSlaveForceTermImplicits id bnd impl tm =

485+ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

486+ideSlaveForceTermImplicits h id bnd impl tm =

458487 do ist <- getIState

459488 let expl = annotate (AnnTerm bnd tm)

460489 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })

@@ -464,7 +493,7 @@ ideSlaveForceTermImplicits id bnd impl tm =

464493 displaySpans .

465494 renderPretty 0.9 80 .

466495 fmap (fancifyAnnots ist) $ expl)

467− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

496+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

468497

469498splitName :: String -> Either String Name

470499splitName s = case reverse $ splitOn "." s of

@@ -473,70 +502,70 @@ splitName s = case reverse $ splitOn "." s of

473502 (n:ns) -> Right $ sNS (sUN n) ns

474503

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

476−ideslaveProcess fn Warranty = process stdout fn Warranty

477−ideslaveProcess fn Help = process stdout fn Help

478−ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

505+ideslaveProcess fn Warranty = process fn Warranty

506+ideslaveProcess fn Help = process fn Help

507+ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

479508 iPrintResult "changed directory to"

480−ideslaveProcess fn (Eval t) = process stdout fn (Eval t)

481−ideslaveProcess fn (NewDefn decls) = do process stdout fn (NewDefn decls)

509+ideslaveProcess fn (Eval t) = process fn (Eval t)

510+ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)

482511 iPrintResult "defined"

483−ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)

484−ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))

485−ideslaveProcess fn (Check t) = process stdout fn (Check t)

486−ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)

487−ideslaveProcess fn Universes = process stdout fn Universes

488−ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)

512+ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)

513+ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

514+ideslaveProcess fn (Check t) = process fn (Check t)

515+ideslaveProcess fn (DocStr n) = process fn (DocStr n)

516+ideslaveProcess fn Universes = process fn Universes

517+ideslaveProcess fn (Defn n) = do process fn (Defn n)

489518 iPrintResult ""

490−ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)

491−ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)

519+ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

520+ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

492521 iPrintResult ""

493−ideslaveProcess fn (Search t) = process stdout fn (Search t)

494−ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

522+ideslaveProcess fn (Search t) = process fn (Search t)

523+ideslaveProcess fn (Spec t) = process fn (Spec t)

495524-- RmProof and AddProof not supported!

496−ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')

497−ideslaveProcess fn (HNF t) = process stdout fn (HNF t)

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

499−ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)

525+ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

526+ideslaveProcess fn (HNF t) = process fn (HNF t)

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

528+ideslaveProcess fn (TestInline t) = process fn (TestInline t)

500529

501−ideslaveProcess fn Execute = do process stdout fn Execute

530+ideslaveProcess fn Execute = do process fn Execute

502531 iPrintResult ""

503−ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)

532+ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

504533 iPrintResult ""

505−ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)

534+ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

506535 iPrintResult ""

507−ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)

508−ideslaveProcess fn (Missing n) = process stdout fn (Missing n)

509−ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)

536+ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

537+ideslaveProcess fn (Missing n) = process fn (Missing n)

538+ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)

510539 iPrintResult ""

511−ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic

540+ideslaveProcess fn ListDynamic = do process fn ListDynamic

512541 iPrintResult ""

513−ideslaveProcess fn Metavars = process stdout fn Metavars

514−ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)

542+ideslaveProcess fn Metavars = process fn Metavars

543+ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

515544 iPrintResult ""

516−ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)

545+ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

517546 iPrintResult ""

518−ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)

547+ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

519548 iPrintResult ""

520−ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)

549+ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

521550 iPrintResult ""

522−ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)

551+ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)

523552 iPrintResult ""

524−ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)

553+ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)

525554 iPrintResult ""

526−ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

527−ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

528−ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)

529−ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)

530−ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)

531−ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)

532−ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)

533−ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)

534−ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

555+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

556+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

557+ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)

558+ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)

559+ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

560+ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

561+ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

562+ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

563+ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

535564 iPrintResult ""

536−ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

565+ideslaveProcess fn (Apropos a) = do process fn (Apropos a)

537566 iPrintResult ""

538−ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)

539−ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)

567+ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)

568+ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)

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

541570

542571

@@ -568,18 +597,18 @@ processInput cmd orig inputs

568597 , idris_colourTheme = idris_colourTheme i

569598 }

570599 clearErr

571− mods <- loadInputs stdout inputs Nothing

600+ mods <- loadInputs inputs Nothing

572601 return (Just inputs)

573602 Success (Load f toline) ->

574603 do putIState orig { idris_options = idris_options i

575604 , idris_colourTheme = idris_colourTheme i

576605 }

577606 clearErr

578− mod <- loadInputs stdout [f] toline

607+ mod <- loadInputs [f] toline

579608 return (Just [f])

580609 Success (ModImport f) ->

581610 do clearErr

582− fmod <- loadModule stdout f

611+ fmod <- loadModule f

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

584613 Success Edit -> do -- takeMVar stvar

585614 edit fn orig

@@ -588,7 +617,7 @@ processInput cmd orig inputs

588617 return (Just inputs)

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

590619 return Nothing

591− Success cmd -> do idrisCatch (process stdout fn cmd)

620+ Success cmd -> do idrisCatch (process fn cmd)

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

593622 return (Just inputs)

594623

@@ -624,7 +653,7 @@ edit f orig

624653 putIState $ orig { idris_options = idris_options i

625654 , idris_colourTheme = idris_colourTheme i

626655 }

627− loadInputs stdout [f] Nothing

656+ loadInputs [f] Nothing

628657-- clearOrigPats

629658 iucheck

630659 return ()

@@ -650,13 +679,13 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

650679 = p : "" : prf : xs

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

652681

653−process :: Handle -> FilePath -> Command -> Idris ()

654−process h fn Help = iPrintResult displayHelp

655−process h fn Warranty = iPrintResult warranty

656−process h fn (ChangeDirectory f)

682+process :: FilePath -> Command -> Idris ()

683+process fn Help = iPrintResult displayHelp

684+process fn Warranty = iPrintResult warranty

685+process fn (ChangeDirectory f)

657686 = do runIO $ setCurrentDirectory f

658687 return ()

659−process h fn (Eval t)

688+process fn (Eval t)

660689 = withErrorReflection $ do logLvl 5 $ show t

661690 (tm, ty) <- elabVal recinfo ERHS t

662691 ctxt <- getContext

@@ -669,10 +698,10 @@ process h fn (Eval t)

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

670699 let tmDoc = pprintDelab ist tm'

671700 tyDoc = pprintDelab ist ty'

672− ihPrintTermWithType h tmDoc tyDoc

701+ iPrintTermWithType tmDoc tyDoc

673702

674703

675−process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ show namedGroups) >> mapM_ defineName namedGroups where

704+process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ show namedGroups) >> mapM_ defineName namedGroups where

676705 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

677706 getName :: PDecl -> Maybe Name

678707 getName (PTy docs argdocs syn fc opts name ty) = Just name

@@ -703,7 +732,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

703732 getRHS (PClauseR fc with rhs whereBlock) = rhs

704733 getRHS (PWithR fc with rhs whereBlock) = rhs

705734

706−process h fn (ExecVal t)

735+process fn (ExecVal t)

707736 = do ctxt <- getContext

708737 ist <- getIState

709738 (tm, ty) <- elabVal recinfo ERHS t

@@ -712,19 +741,19 @@ process h fn (ExecVal t)

712741 res <- execute tm

713742 let (resOut, tyOut) = (prettyIst ist (delab ist res),

714743 prettyIst ist (delab ist ty'))

715− ihPrintTermWithType h resOut tyOut

744+ iPrintTermWithType resOut tyOut

716745

717−process h fn (Check (PRef _ n))

746+process fn (Check (PRef _ n))

718747 = do ctxt <- getContext

719748 ist <- getIState

720749 let ppo = ppOptionIst ist

721750 case lookupNames n ctxt of

722751 ts@(t:_) ->

723752 case lookup t (idris_metavars ist) of

724− Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

753+ Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $

725754 showMetavarInfo ppo ist n i

726− Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

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

755+ Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)

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

728757 where

729758 showMetavarInfo ppo ist n i

730759 = case lookupTy n (tt_ctxt ist) of

@@ -749,7 +778,7 @@ process h fn (Check (PRef _ n))

749778 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

750779

751780

752−process h fn (Check t)

781+process fn (Check t)

753782 = do (tm, ty) <- elabVal recinfo ERHS t

754783 ctxt <- getContext

755784 ist <- getIState

@@ -757,24 +786,24 @@ process h fn (Check t)

757786 ty' = normaliseC ctxt [] ty

758787 case tm of

759788 TType _ ->

760− ihPrintTermWithType h (prettyIst ist PType) type1Doc

761− _ -> ihPrintTermWithType h (pprintDelab ist tm)

762− (pprintDelab ist ty)

789+ iPrintTermWithType (prettyIst ist PType) type1Doc

790+ _ -> iPrintTermWithType (pprintDelab ist tm)

791+ (pprintDelab ist ty)

763792

764−process h fn (DocStr (Left n))

793+process fn (DocStr (Left n))

765794 = do ist <- getIState

766795 case lookupCtxtName n (idris_docstrings ist) of

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

768797 ns -> do toShow <- mapM (showDoc ist) ns

769− ihRenderResult h (vsep toShow)

798+ iRenderResult (vsep toShow)

770799 where showDoc ist (n, d) = do doc <- getDocs n

771800 return $ pprintDocs ist doc

772801

773−process h fn (DocStr (Right c))

802+process fn (DocStr (Right c))

774803 = do ist <- getIState

775− ihRenderResult h $ pprintConstDocs ist c (constDocs c)

804+ iRenderResult $ pprintConstDocs ist c (constDocs c)

776805

777−process h fn Universes

806+process fn Universes

778807 = do i <- getIState

779808 let cs = idris_constraints i

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

@@ -784,7 +813,7 @@ process h fn Universes

784813 case ucheck cs of

785814 Error e -> iPrintError $ pshow i e

786815 OK _ -> iPrintResult "Universes OK"

787−process h fn (Defn n)

816+process fn (Defn n)

788817 = do i <- getIState

789818 iputStrLn "Compiled patterns:\n"

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

@@ -799,20 +828,20 @@ process h fn (Defn n)

799828 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

800829 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

801830 showTm i' (delab i rhs))

802−process h fn (TotCheck n)

831+process fn (TotCheck n)

803832 = do i <- getIState

804833 case lookupNameTotal n (tt_ctxt i) of

805− [] -> ihPrintError h $ "Unknown operator " ++ show n

834+ [] -> iPrintError $ "Unknown operator " ++ show n

806835 ts -> do ist <- getIState

807836 c <- colourise

808837 let ppo = ppOptionIst ist

809838 let showN = showName (Just ist) [] ppo c

810− ihPrintResult h . concat . intersperse "\n" .

839+ iPrintResult . concat . intersperse "\n" .

811840 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

812841 ts

813842

814843

815−process h fn (DebugInfo n)

844+process fn (DebugInfo n)

816845 = do i <- getIState

817846 let oi = lookupCtxtName n (idris_optimisation i)

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

@@ -829,29 +858,29 @@ process h fn (DebugInfo n)

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

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

831860 iputStrLn (show cg')

832−process h fn (Search t) = searchByType h t

833−process h fn (CaseSplitAt updatefile l n)

834− = caseSplitAt h fn updatefile l n

835−process h fn (AddClauseFrom updatefile l n)

836− = addClauseFrom h fn updatefile l n

837−process h fn (AddProofClauseFrom updatefile l n)

838− = addProofClauseFrom h fn updatefile l n

839−process h fn (AddMissing updatefile l n)

840− = addMissing h fn updatefile l n

841−process h fn (MakeWith updatefile l n)

842− = makeWith h fn updatefile l n

843−process h fn (MakeLemma updatefile l n)

844− = makeLemma h fn updatefile l n

845−process h fn (DoProofSearch updatefile rec l n hints)

846− = doProofSearch h fn updatefile rec l n hints Nothing

847−process h fn (Spec t)

861+process fn (Search t) = searchByType t

862+process fn (CaseSplitAt updatefile l n)

863+ = caseSplitAt fn updatefile l n

864+process fn (AddClauseFrom updatefile l n)

865+ = addClauseFrom fn updatefile l n

866+process fn (AddProofClauseFrom updatefile l n)

867+ = addProofClauseFrom fn updatefile l n

868+process fn (AddMissing updatefile l n)

869+ = addMissing fn updatefile l n

870+process fn (MakeWith updatefile l n)

871+ = makeWith fn updatefile l n

872+process fn (MakeLemma updatefile l n)

873+ = makeLemma fn updatefile l n

874+process fn (DoProofSearch updatefile rec l n hints)

875+ = doProofSearch fn updatefile rec l n hints Nothing

876+process fn (Spec t)

848877 = do (tm, ty) <- elabVal recinfo ERHS t

849878 ctxt <- getContext

850879 ist <- getIState

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

852881 iPrintResult (show (delab ist tm'))

853882

854−process h fn (RmProof n')

883+process fn (RmProof n')

855884 = do i <- getIState

856885 n <- resolveProof n'

857886 let proofs = proof_list i

@@ -867,7 +896,7 @@ process h fn (RmProof n')

867896 let ms = idris_metavars i

868897 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

869898

870−process h fn' (AddProof prf)

899+process fn' (AddProof prf)

871900 = do fn <- do

872901 let fn'' = takeWhile (/= ' ') fn'

873902 ex <- runIO $ doesFileExist fn''

@@ -897,7 +926,7 @@ process h fn' (AddProof prf)

897926 iputStrLn $ "Added proof " ++ show n

898927 where ls = (lines prog)

899928

900−process h fn (ShowProof n')

929+process fn (ShowProof n')

901930 = do i <- getIState

902931 n <- resolveProof n'

903932 let proofs = proof_list i

@@ -905,7 +934,7 @@ process h fn (ShowProof n')

905934 Nothing -> iPrintError "No proof to show"

906935 Just p -> iPrintResult $ showProof False n p

907936

908−process h fn (Prove n')

937+process fn (Prove n')

909938 = do ctxt <- getContext

910939 ist <- getIState

911940 let ns = lookupNames n' ctxt

@@ -923,20 +952,20 @@ process h fn (Prove n')

923952 mapM_ checkDeclTotality (idris_totcheck i)

924953 warnTotality

925954

926−process h fn (HNF t)

955+process fn (HNF t)

927956 = do (tm, ty) <- elabVal recinfo ERHS t

928957 ctxt <- getContext

929958 ist <- getIState

930959 let tm' = hnf ctxt [] tm

931960 iPrintResult (show (delab ist tm'))

932−process h fn (TestInline t)

961+process fn (TestInline t)

933962 = do (tm, ty) <- elabVal recinfo ERHS t

934963 ctxt <- getContext

935964 ist <- getIState

936965 let tm' = inlineTerm ist tm

937966 c <- colourise

938967 iPrintResult (showTm ist (delab ist tm'))

939−process h fn Execute

968+process fn Execute

940969 = idrisCatch

941970 (do ist <- getIState

942971 (m, _) <- elabVal recinfo ERHS

@@ -948,33 +977,33 @@ process h fn Execute

948977 t <- codegen

949978 compile t tmpn m

950979 case idris_outputmode ist of

951− RawOutput -> do runIO $ system tmpn

952− return ()

953− IdeSlave n -> runIO . hPutStrLn h $

954− IdeSlave.convSExp "run-program" tmpn n)

955− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

980+ RawOutput h -> do runIO $ system tmpn

981+ return ()

982+ IdeSlave n h -> runIO . hPutStrLn h $

983+ IdeSlave.convSExp "run-program" tmpn n)

984+ (\e -> getIState >>= iRenderError . flip pprintErr e)

956985 where fc = fileFC "main"

957−process h fn (Compile codegen f)

986+process fn (Compile codegen f)

958987 = do (m, _) <- elabVal recinfo ERHS

959988 (PApp fc (PRef fc (sUN "run__IO"))

960989 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

961990 compile codegen f m

962991 where fc = fileFC "main"

963−process h fn (LogLvl i) = setLogLevel i

992+process fn (LogLvl i) = setLogLevel i

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

965−process h fn (Pattelab t)

994+process fn (Pattelab t)

966995 = do (tm, ty) <- elabVal recinfo ELHS t

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

968997

969−process h fn (Missing n)

998+process fn (Missing n)

970999 = do i <- getIState

9711000 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

9721001 case lookupCtxt n (idris_patdefs i) of

973− [] -> ihPrintError h $ "Unknown operator " ++ show n

1002+ [] -> iPrintError $ "Unknown operator " ++ show n

9741003 [(_, tms)] ->

9751004 iPrintResult (showSep "\n" (map (showTm i') tms))

9761005 _ -> iPrintError $ "Ambiguous name"

977−process h fn (DynamicLink l)

1006+process fn (DynamicLink l)

9781007 = do i <- getIState

9791008 let importdirs = opt_importdirs (idris_options i)

9801009 lib = trim l

@@ -987,80 +1016,80 @@ process h fn (DynamicLink l)

9871016 return ()

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

9891018 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

990−process h fn ListDynamic

1019+process fn ListDynamic

9911020 = do i <- getIState

9921021 iputStrLn "Dynamic libraries:"

9931022 showLibs $ idris_dynamic_libs i

9941023 where showLibs [] = return ()

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

996−process h fn Metavars

1025+process fn Metavars

9971026 = do ist <- getIState

9981027 let mvs = map fst (idris_metavars ist) \\ primDefs

9991028 case mvs of

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

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

1002−process h fn NOP = return ()

1003−

1004−process h fn (SetOpt ErrContext) = setErrContext True

1005−process h fn (UnsetOpt ErrContext) = setErrContext False

1006−process h fn (SetOpt ShowImpl) = setImpShow True

1007−process h fn (UnsetOpt ShowImpl) = setImpShow False

1008−process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

1009−process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1010−process h fn (SetOpt AutoSolve) = setAutoSolve True

1011−process h fn (UnsetOpt AutoSolve) = setAutoSolve False

1012−process h fn (SetOpt NoBanner) = setNoBanner True

1013−process h fn (UnsetOpt NoBanner) = setNoBanner False

1014−process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1015−process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1016−

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

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

1019−process h fn (SetColour ty c) = setColour ty c

1020−process h fn ColourOn

1031+process fn NOP = return ()

1032+

1033+process fn (SetOpt ErrContext) = setErrContext True

1034+process fn (UnsetOpt ErrContext) = setErrContext False

1035+process fn (SetOpt ShowImpl) = setImpShow True

1036+process fn (UnsetOpt ShowImpl) = setImpShow False

1037+process fn (SetOpt ShowOrigErr) = setShowOrigErr True

1038+process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1039+process fn (SetOpt AutoSolve) = setAutoSolve True

1040+process fn (UnsetOpt AutoSolve) = setAutoSolve False

1041+process fn (SetOpt NoBanner) = setNoBanner True

1042+process fn (UnsetOpt NoBanner) = setNoBanner False

1043+process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1044+process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1045+

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

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

1048+process fn (SetColour ty c) = setColour ty c

1049+process fn ColourOn

10211050 = do ist <- getIState

10221051 putIState $ ist { idris_colourRepl = True }

1023−process h fn ColourOff

1052+process fn ColourOff

10241053 = do ist <- getIState

10251054 putIState $ ist { idris_colourRepl = False }

1026−process h fn ListErrorHandlers =

1055+process fn ListErrorHandlers =

10271056 do ist <- getIState

10281057 iPrintResult $ case idris_errorhandlers ist of

10291058 [] -> "No registered error handlers"

10301059 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

1031−process h fn (SetConsoleWidth w) = setWidth w

1060+process fn (SetConsoleWidth w) = setWidth w

10321061

1033−process h fn (Apropos a) =

1062+process fn (Apropos a) =

10341063 do ist <- getIState

10351064 let names = apropos ist (T.pack a)

10361065 let aproposInfo = [ (n,

10371066 delabTy ist n,

10381067 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

10391068 | n <- sort names, isUN n ]

1040− ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1069+ iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)

10411070 where isUN (UN _) = True

10421071 isUN (NS n _) = isUN n

10431072 isUN _ = False

10441073

1045−process h fn (WhoCalls n) =

1074+process fn (WhoCalls n) =

10461075 do calls <- whoCalls n

10471076 ist <- getIState

1048− ihRenderResult h . vsep $

1077+ iRenderResult . vsep $

10491078 map (\(n, ns) ->

10501079 text "Callers of" <+> prettyName True True [] n <$>

10511080 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

10521081 calls

10531082

1054−process h fn (CallsWho n) =

1083+process fn (CallsWho n) =

10551084 do calls <- callsWho n

10561085 ist <- getIState

1057− ihRenderResult h . vsep $

1086+ iRenderResult . vsep $

10581087 map (\(n, ns) ->

10591088 prettyName True True [] n <+> text "calls:" <$>

10601089 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

10611090 calls

10621091-- IdrisDoc

1063−process h fn (MakeDoc s) =

1092+process fn (MakeDoc s) =

10641093 do istate <- getIState

10651094 let names = words s

10661095 parse n | Success x <- runparser name istate fn n = Right x

@@ -1117,8 +1146,8 @@ idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

11171146 [] -> return ()

11181147

11191148

1120−loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()

1121−loadInputs h inputs toline -- furthest line to read in input source files

1149+loadInputs :: [FilePath] -> Maybe Int -> Idris ()

1150+loadInputs inputs toline -- furthest line to read in input source files

11221151 = idrisCatch

11231152 (do ist <- getIState

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

@@ -1170,10 +1199,10 @@ loadInputs h inputs toline -- furthest line to read in input source files

11701199 (\e -> do i <- getIState

11711200 case e of

11721201 At f e' -> do setErrSpan f

1173− ihWarn stdout f $ pprintErr i e'

1202+ iWarn f $ pprintErr i e'

11741203 ProgramLineComment -> return () -- fail elsewhere

11751204 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1176− ihWarn stdout emptyFC $ pprintErr i e)

1205+ iWarn emptyFC $ pprintErr i e)

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

11781207 tryLoad :: Bool -> [IFileType] -> Idris ()

11791208 tryLoad keepstate [] = warnTotality >> return ()

@@ -1190,7 +1219,7 @@ loadInputs h inputs toline -- furthest line to read in input source files

11901219 then Just l

11911220 else Nothing

11921221 _ -> Nothing

1193− loadFromIFile h f maxline

1222+ loadFromIFile f maxline

11941223 inew <- getIState

11951224 -- FIXME: Save these in IBC to avoid this hack! Need to

11961225 -- preserve it all from source inputs

@@ -1238,7 +1267,7 @@ idrisMain opts =

12381267 do let inputs = opt getFile opts

12391268 let quiet = Quiet `elem` opts

12401269 let nobanner = NoBanner `elem` opts

1241− let idesl = Ideslave `elem` opts

1270+ let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts

12421271 let runrepl = not (NoREPL `elem` opts)

12431272 let verbose = runrepl || Verbose `elem` opts

12441273 let output = opt getOutput opts

@@ -1275,7 +1304,6 @@ idrisMain opts =

12751304 mapM_ addLangExt (opt getLanguageExt opts)

12761305 setREPL runrepl

12771306 setQuiet (quiet || isJust script || not (null immediate))

1278− setIdeSlave idesl

12791307 setVerbose verbose

12801308 setCmdLine opts

12811309 setOutputTy outty

@@ -1301,9 +1329,9 @@ idrisMain opts =

13011329 addPkgDir "base"

13021330 mapM_ addPkgDir pkgdirs

13031331 elabPrims

1304− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"

1332+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"

13051333 return ()

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

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

13071335 return ()

13081336

13091337 when (runrepl && not idesl) initScript

@@ -1319,14 +1347,14 @@ idrisMain opts =

13191347 iputStrLn banner

13201348

13211349 orig <- getIState

1322− loadInputs stdout inputs Nothing

1350+ when (not idesl) $ loadInputs inputs Nothing

13231351

13241352 runIO $ hSetBuffering stdout LineBuffering

13251353

13261354 ok <- noErrors

13271355 when ok $ case output of

13281356 [] -> return ()

1329− (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1357+ (o:_) -> idrisCatch (process "" (Compile cgn o))

13301358 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

13311359

13321360 case immediate of

@@ -1337,7 +1365,7 @@ idrisMain opts =

13371365 case parseExpr ist str of

13381366 Failure err -> do iputStrLn $ show (fixColour c err)

13391367 runIO $ exitWith (ExitFailure 1)

1340− Success e -> process stdout "" (Eval e))

1368+ Success e -> process "" (Eval e))

13411369 exprs

13421370 runIO $ exitWith ExitSuccess

13431371

@@ -1359,7 +1387,8 @@ idrisMain opts =

13591387-- clearOrigPats

13601388 startServer orig inputs

13611389 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1362− when (idesl) $ ideslaveStart orig inputs

1390+ let idesock = IdeslaveSocket `elem` opts

1391+ when (idesl) $ ideslaveStart idesock orig inputs

13631392 ok <- noErrors

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

13651394 where

@@ -1421,7 +1450,7 @@ initScript = do script <- getInitScript

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

14221451 Success Proofs -> proofs i

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

1424− Success cmd -> process stdout [] cmd

1453+ Success cmd -> process [] cmd

14251454

14261455getFile :: Opt -> Maybe String

14271456getFile (Filename str) = Just str

src/Idris/TypeSearch.hs+6−8

@@ -29,14 +29,12 @@ import Idris.Core.Unify (match_unify)

2929import Idris.Delaborate (delabTy)

3030import Idris.Docstrings (noDocs, overview)

3131import Idris.Elab.Type (elabType)

32−import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)

33−

34−import System.IO (Handle)

32+import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)

3533

3634import Util.Pretty (text, char, vsep, (<>), Doc)

3735

38−searchByType :: Handle -> PTerm -> Idris ()

39−searchByType h pterm = do

36+searchByType :: PTerm -> Idris ()

37+searchByType pterm = do

4038 pterm' <- addUsingConstraints syn emptyFC pterm

4139 pterm'' <- implicit toplevel syn n pterm'

4240 i <- getIState

@@ -50,9 +48,9 @@ searchByType h pterm = do

5048 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

5149 | (n, score) <- names']

5250 case idris_outputmode i of

53− RawOutput -> do mapM_ (ihRenderOutput h) docs

54− ihPrintResult h ""

55− IdeSlave n -> ihRenderResult h (vsep docs)

51+ RawOutput _ -> do mapM_ iRenderOutput docs

52+ iPrintResult ""

53+ IdeSlave n h -> iRenderResult (vsep docs)

5654 where

5755 numLimit = 50

5856 syn = defaultSyntax { implicitAllowed = True } -- syntax

src/Pkg/Package.hs+1−1

@@ -144,7 +144,7 @@ documentPkg fp =

144144 setCurrentDirectory $ pkgDir

145145 let run l = runErrorT . (execStateT l)

146146 load [] = return ()

147− load (f:fs) = do loadModule stdout f; load fs

147+ load (f:fs) = do loadModule f; load fs

148148 loader = do idrisMain opts; load fs

149149 idrisInstance <- run loader idrisInit

150150 setCurrentDirectory cd

src/Util/Net.hs+15−2

@@ -1,6 +1,6 @@

1−module Util.Net (listenOnLocalhost) where

1+module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where

3−import Network

3+import Network hiding (socketPort)

44import Network.Socket hiding (sClose, PortNumber)

55import Network.BSD (getProtocolNumber)

66import Control.Exception (bracketOnError)

@@ -20,3 +20,16 @@ listenOnLocalhost (PortNumber port) = do

2020 return sock

2121 )

2222

23+listenOnLocalhostAnyPort = do

24+ proto <- getProtocolNumber "tcp"

25+ localhost <- inet_addr "127.0.0.1"

26+ bracketOnError

27+ (socket AF_INET Stream proto)

28+ (sClose)

29+ (\sock -> do

30+ setSocketOption sock ReuseAddr 1

31+ bindSocket sock (SockAddrInet aNY_PORT localhost)

32+ listen sock maxListenQueue

33+ port <- socketPort sock

34+ return (sock, port)

35+ )