d947282 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1452 from hannesm/ideslave-socket

d947282David Christiansen12 years ago

src/Idris/AbsSyntax.hs+10−14

compare with master

unifiedsplit

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

537isetPrompt :: String -> Idris ()

538isetPrompt p = do i <- getIState

539 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

541

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

543isetLoadedRegion :: Idris ()

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

546 case span of

547 Just fc ->

548 case idris_outputmode i of

549− IdeSlave n ->

549+ IdeSlave n h ->

550− runIO . putStrLn $

550+ runIO . hPutStrLn h $

551 convSExp "set-loaded-region" fc n

552 Nothing -> return ()

553

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

662outputTy = do i <- getIState

663 return $ opt_outputTy $ idris_options i

664

665−setIdeSlave :: Bool -> Idris ()

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

666−setIdeSlave True = do i <- getIState

666+setIdeSlave True h = do i <- getIState

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

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

668−setIdeSlave False = return ()

668+setIdeSlave False _ = return ()

669

670setTargetTriple :: String -> Idris ()

671setTargetTriple t = do i <- getIState

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

761setColourise b = do i <- getIState

762 putIState $ i { idris_colourRepl = b }

763

764−setOutH :: Handle -> Idris ()

765−setOutH h = do i <- getIState

766− putIState $ i { idris_outh = h }

767−

768impShow :: Idris Bool

764impShow :: Idris Bool

769impShow = do i <- getIState

765impShow = do i <- getIState

770 return (opt_showimp (idris_options i))

766 return (opt_showimp (idris_options i))

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

793 let lvl = opt_logLevel (idris_options i)

789 let lvl = opt_logLevel (idris_options i)

794 when (lvl >= l) $

790 when (lvl >= l) $

795 case idris_outputmode i of

791 case idris_outputmode i of

796− RawOutput -> do runIO $ putStrLn str

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

797− IdeSlave n ->

793+ IdeSlave n h ->

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

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

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

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

800

796

801cmdOptType :: Opt -> Idris Bool

797cmdOptType :: Opt -> Idris Bool

802cmdOptType x = do i <- getIState

798cmdOptType x = do i <- getIState

src/Idris/AbsSyntaxTree.hs+6−4

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

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

128

129-- | 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

131

133

132-- | How wide is the console?

134-- | How wide is the console?

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

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

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

192 idris_outputmode :: OutputMode,

194 idris_outputmode :: OutputMode,

193 idris_colourRepl :: Bool,

195 idris_colourRepl :: Bool,

194 idris_colourTheme :: ColourTheme,

196 idris_colourTheme :: ColourTheme,

195− idris_outh :: Handle,

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

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

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

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

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

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

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

277 emptyContext emptyContext emptyContext emptyContext

278 emptyContext emptyContext emptyContext emptyContext

278 emptyContext emptyContext

279 emptyContext emptyContext

279 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

280 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

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

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

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

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

282 AutomaticWidth S.empty Nothing Nothing

283 AutomaticWidth S.empty Nothing Nothing

283

284

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

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

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

358 | NoBanner

359 | NoBanner

359 | ColourREPL Bool

360 | ColourREPL Bool

360 | Ideslave

361 | Ideslave

362+ | IdeslaveSocket

361 | ShowLibs

363 | ShowLibs

362 | ShowLibdir

364 | ShowLibdir

363 | ShowIncs

365 | ShowIncs

src/Idris/CmdOptions.hs+1

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Error.hs+2−3

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

43setAndReport :: Err -> Idris ()

44setAndReport e = do ist <- getIState

45− let h = idris_outh ist

46 case (unwrap e) of

45 case (unwrap e) of

47 At fc e -> do setErrSpan fc

46 At fc e -> do setErrSpan fc

48− ihWarn h fc $ pprintErr ist e

47+ iWarn fc $ pprintErr ist e

49 _ -> do setErrSpan (getErrSpan e)

48 _ -> do setErrSpan (getErrSpan e)

50− ihWarn h emptyFC $ pprintErr ist e

49+ iWarn emptyFC $ pprintErr ist e

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

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

52 unwrap e = e

51 unwrap e = e

src/Idris/IdeSlave.hs+20−10

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

1{-# 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

5import Text.Printf

6import Numeric

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

12-- import qualified Data.Text as T

13import Text.Trifecta hiding (Err)

14import Text.Trifecta.Delta

15+import System.IO

16import Idris.Core.TT

17import Idris.Core.TT

17import Idris.Core.Binary

18import Idris.Core.Binary

19import Control.Applicative hiding (Const)

20import Control.Applicative hiding (Const)

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+

21data SExp = SexpList [SExp]

33data SExp = SexpList [SExp]

22 | StringAtom String

34 | StringAtom String

23 | BoolAtom Bool

35 | BoolAtom Bool

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

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

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

248parseMessage x = case receiveString x of

260parseMessage x = case receiveString x of

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

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

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

250 Left err -> Left err

263 Left err -> Left err

251

264

252receiveString :: String -> Either Err SExp

265receiveString :: String -> Either Err SExp

253receiveString x =

266receiveString 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

267+ case parseSExp x of

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

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

261− Success r -> Right r)

269+ Success r -> Right r

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

263

270

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

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

265convSExp pre s id =

272convSExp pre s id =

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

269

276

270getHexLength :: String -> String

277getHexLength :: String -> String

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

278getHexLength 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)

32import Debug.Trace

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

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

35−caseSplitAt h fn updatefile l n

35+caseSplitAt fn updatefile l n

36 = do src <- runIO $ readFile fn

37 res <- splitOnLine l n fn

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

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

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

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

45 runIO $ copyFile fb fn

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

46+ else -- do iputStrLn (show res)

47− ihPrintResult h new

47+ iPrintResult new

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

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

50−addClauseFrom h fn updatefile l n

50+addClauseFrom fn updatefile l n

51 = do src <- runIO $ readFile fn

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

53 let indent = getIndent 0 (show n) tyline

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

61 cl ++ "\n" ++

62 unlines rest)

63 runIO $ copyFile fb fn

64− else ihPrintResult h cl

64+ else iPrintResult cl

65 where

66 getIndent i n [] = 0

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

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

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

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

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

72−addProofClauseFrom h fn updatefile l n

72+addProofClauseFrom fn updatefile l n

73 = do src <- runIO $ readFile fn

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

75 let indent = getIndent 0 (show n) tyline

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

83 cl ++ "\n" ++

84 unlines rest)

85 runIO $ copyFile fb fn

86− else ihPrintResult h cl

86+ else iPrintResult cl

87 where

88 getIndent i n [] = 0

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

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

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

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

93−addMissing h fn updatefile l n

93+addMissing fn updatefile l n

94 = do src <- runIO $ readFile fn

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

96 let indent = getIndent 0 (show n) tyline

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

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

109 ++ extras ++ unlines rest)

110 runIO $ copyFile fb fn

111− else ihPrintResult h extras

111+ else iPrintResult extras

112 where showPat = show . stripNS

113 stripNS tm = mapPT dens tm where

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

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

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

136

137

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

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

139−makeWith h fn updatefile l n

139+makeWith fn updatefile l n

140 = do src <- runIO $ readFile fn

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

142 let ind = getIndent tyline

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

151 ++ with ++ "\n" ++

152 unlines rest)

153 runIO $ copyFile fb fn

154− else ihPrintResult h with

154+ else iPrintResult with

155 where getIndent s = length (takeWhile isSpace s)

156

157

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

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

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

160−doProofSearch h fn updatefile rec l n hints Nothing

160+doProofSearch fn updatefile rec l n hints Nothing

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

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

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

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

163 = do src <- runIO $ readFile fn

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

165 ctxt <- getContext

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

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

193 ++ unlines later)

194 runIO $ copyFile fb fn

195− else ihPrintResult h newmv

195+ else iPrintResult newmv

196 where dropCtxt 0 sc = sc

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

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

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

235 | otherwise = new

236

237

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

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

239−makeLemma h fn updatefile l n

239+makeLemma fn updatefile l n

240 = do src <- runIO $ readFile fn

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

242

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

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

267 runIO $ copyFile fb fn

268 else case idris_outputmode i of

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

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

270− IdeSlave n ->

270+ IdeSlave n h ->

271 let good = SexpList [SymbolAtom "ok",

272 SexpList [SymbolAtom "metavariable-lemma",

273 SexpList [SymbolAtom "replace-metavariable",

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

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

285 runIO $ copyFile fb fn

286 else case idris_outputmode i of

287− RawOutput -> ihPrintResult h $ lem_app

287+ RawOutput _ -> iPrintResult $ lem_app

288− IdeSlave n ->

288+ IdeSlave n h ->

289 let good = SexpList [SymbolAtom "ok",

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

291 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+60−63

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

24 renderPretty 1.0 80 .

25 fmap (fancifyAnnots ist) $ pprintErr ist err

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

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

28+iWarn fc err =

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

29+ do i <- getIState

29− case idris_outputmode i of

30+ case idris_outputmode i of

30− RawOutput ->

31+ RawOutput h ->

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

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

32− if fc_fname fc /= ""

33+ if fc_fname fc /= ""

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

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

34− else err

35+ else err

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

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

36− IdeSlave n ->

37+ IdeSlave n h ->

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

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

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

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

39− runIO . hPutStrLn h $

40+ runIO . hPutStrLn h $

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

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

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

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

43iRender d = do w <- getWidth

44iRender d = do w <- getWidth

44 ist <- getIState

45 ist <- getIState

45 let ideSlave = case idris_outputmode ist of

46 let ideSlave = case idris_outputmode ist of

46− IdeSlave _ -> True

47+ IdeSlave _ _ -> True

47− _ -> False

48+ _ -> False

48 case w of

49 case w of

49 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

50 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

50 ColsWide n -> return $

51 ColsWide n -> return $

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

63 displayDecorated (consoleDecorate ist) $

64 displayDecorated (consoleDecorate ist) $

64 rendered

65 rendered

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

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

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

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

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

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

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

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

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

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

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

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

73− let ppo = ppOptionIst ist

74+ let ppo = ppOptionIst ist

74− let infixes = idris_infixes ist

75+ let infixes = idris_infixes ist

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

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

76− ihRenderResult h output

77+ iRenderResult output

77 where fullName n = prettyName True True bnd n

78 where fullName n = prettyName True True bnd n

78 ppOverload ppo infixes n tm =

79 ppOverload ppo infixes n tm =

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

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

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

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

82−ihRenderOutput h doc =

83+iRenderOutput doc =

83 do i <- getIState

84 do i <- getIState

84 case idris_outputmode i of

85 case idris_outputmode i of

85− RawOutput -> do out <- iRender doc

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

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

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

87− IdeSlave n ->

88+ IdeSlave n h ->

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

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

89 let out = [toSExp str, toSExp spans]

90 let out = [toSExp str, toSExp spans]

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

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

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

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

93−ihRenderResult h d = do ist <- getIState

94+iRenderResult d = do ist <- getIState

94− case idris_outputmode ist of

95+ case idris_outputmode ist of

95− RawOutput -> consoleDisplayAnnotated h d

96+ RawOutput h -> consoleDisplayAnnotated h d

96− IdeSlave n -> ideSlaveReturnAnnotated n h d

97+ IdeSlave n h -> ideSlaveReturnAnnotated n h d

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

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

99ideSlaveReturnWithStatus status n h out = do

100ideSlaveReturnWithStatus status n h out = do

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

111ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

112ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

112

113

113-- | Show an error with semantic highlighting

114-- | Show an error with semantic highlighting

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

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

115−ihRenderError h e = do ist <- getIState

116+iRenderError e = do ist <- getIState

116− case idris_outputmode ist of

117+ case idris_outputmode ist of

117− RawOutput -> consoleDisplayAnnotated h e

118+ RawOutput h -> consoleDisplayAnnotated h e

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

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

119−

120+

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

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

121−ihPrintWithStatus status h s = do

122+iPrintWithStatus status s = do

122 i <- getIState

123 i <- getIState

123 case idris_outputmode i of

124 case idris_outputmode i of

124− RawOutput -> case s of

125+ RawOutput h -> case s of

125 "" -> return ()

126 "" -> return ()

126 s -> runIO $ hPutStrLn h s

127 s -> runIO $ hPutStrLn h s

127− IdeSlave n ->

128+ IdeSlave n h ->

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

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

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

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

130

131

132

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

133+iPrintResult :: String -> Idris ()

133−ihPrintResult = ihPrintWithStatus "ok"

134+iPrintResult = iPrintWithStatus "ok"

134

135

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

136+iPrintError :: String -> Idris ()

136−ihPrintError = ihPrintWithStatus "error"

137+iPrintError = iPrintWithStatus "error"

137

138

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

139+iputStrLn :: String -> Idris ()

139−ihputStrLn h s = do i <- getIState

140+iputStrLn s = do i <- getIState

140− case idris_outputmode i of

141+ case idris_outputmode i of

141− RawOutput -> runIO $ hPutStrLn h s

142+ RawOutput h -> runIO $ hPutStrLn h s

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

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

143

144

144−iputStrLn = ihputStrLn stdout

145−iPrintError = ihPrintError stdout

146−iPrintResult = ihPrintResult stdout

147−iWarn = ihWarn stdout

148

145

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

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

150ideslavePutSExp cmd info = do i <- getIState

147ideslavePutSExp cmd info = do i <- getIState

151 case idris_outputmode i of

148 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

153 _ -> return ()

150 _ -> return ()

154

151

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

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

156iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

153iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

157iputGoal g = do i <- getIState

154iputGoal g = do i <- getIState

158 case idris_outputmode i of

155 case idris_outputmode i of

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

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

160− IdeSlave n ->

157+ IdeSlave n h ->

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

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

162 goal = [toSExp str, toSExp spans]

159 goal = [toSExp str, toSExp spans]

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

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

164

161

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

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

166warnTotality :: Idris ()

163warnTotality :: Idris ()

src/Idris/ParseHelpers.hs+2−2

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

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19import Idris.Docstrings

20−import Idris.Output (ihWarn)

20+import Idris.Output (iWarn)

22import qualified Util.Pretty as Pretty (text)

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

80reportParserWarnings :: Idris ()

81reportParserWarnings = do ist <- getIState

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

82+ mapM_ (uncurry iWarn)

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

84 reverse .

85 nub $

src/Idris/Parser.hs+24−24

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

1159 let (fc, msg) = findFC doc

1160 i <- getIState

1161 case idris_outputmode i of

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

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

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

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

1164 putIState (i { errSpan = Just fc })

1165 return []

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

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

1176 return (ds, i')

1177

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

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

1179+loadModule :: FilePath -> Idris String

1180−loadModule outh f

1180+loadModule f

1181− = idrisCatch (loadModule' outh f)

1181+ = idrisCatch (loadModule' f)

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

1183 ist <- getIState

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

1184+ iWarn (getErrSpan e) $ pprintErr ist e

1185 return "")

1186

1187{- | Load idris module -}

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

1188+loadModule' :: FilePath -> Idris String

1189−loadModule' outh f

1189+loadModule' f

1190 = do i <- getIState

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

1192 ibcsd <- valIBCSubDir i

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

1196 then iLOG $ "Already read " ++ file

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

1198 case fp of

1199− IDR fn -> loadSource outh False fn Nothing

1199+ IDR fn -> loadSource False fn Nothing

1200− LIDR fn -> loadSource outh True fn Nothing

1200+ LIDR fn -> loadSource True fn Nothing

1201 IBC fn src ->

1202 idrisCatch (loadIBC fn)

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

1204 case src of

1205− IDR sfn -> loadSource outh False sfn Nothing

1205+ IDR sfn -> loadSource False sfn Nothing

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

1206+ LIDR sfn -> loadSource True sfn Nothing)

1207 let (dir, fh) = splitFileName file

1208 return (dropExtension fh)

1209

1210

1211{- | Load idris code from file -}

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

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

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

1213+loadFromIFile i@(IBC fn src) maxline

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

1215 idrisCatch (loadIBC fn)

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

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

1219 getSrcFile (LIDR fn) = fn

1220 getSrcFile (IBC f src) = getSrcFile src

1221

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

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

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

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

1224

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

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

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

1227−loadSource' h lidr r maxline

1227+loadSource' lidr r maxline

1228− = idrisCatch (loadSource h lidr r maxline)

1228+ = idrisCatch (loadSource lidr r maxline)

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

1230 ist <- getIState

1231 case e of

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

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

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

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

1234

1235{- | Load Idris source code-}

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

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

1237−loadSource h lidr f toline

1237+loadSource lidr f toline

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

1239 i <- getIState

1240 let def_total = default_total i

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

1278 logLvl 3 (show (idris_infixes i))

1279 -- Now add all the declarations to the context

1280 v <- verbose

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

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

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

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

1284 -- mutual block on its own

src/Idris/Prover.hs+46−45

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

19import Idris.Error

20import Idris.DataOpts

21import Idris.Completion

22−import Idris.IdeSlave

22+import qualified Idris.IdeSlave as IdeSlave

23import Idris.Output

24import Idris.TypeSearch (searchByType)

26import Text.Trifecta.Result(Result(..))

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

28import System.Console.Haskeline

29import System.Console.Haskeline

29import System.Console.Haskeline.History

30import System.Console.Haskeline.History

30import Control.Monad.State.Strict

31import Control.Monad.State.Strict

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

70 iLOG $ "Adding " ++ show tm

71 iLOG $ "Adding " ++ show tm

71 i <- getIState

72 i <- getIState

72 case idris_outputmode i of

73 case idris_outputmode i of

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

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

74− _ -> iputStrLn $ showProof lit n prf

75+ _ -> iputStrLn $ showProof lit n prf

75 let proofs = proof_list i

76 let proofs = proof_list i

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

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

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

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

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

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

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

94 solveDeferred n

95 solveDeferred n

95 case idris_outputmode i of

96 case idris_outputmode i of

96− IdeSlave n ->

97+ IdeSlave n h ->

97− runIO . putStrLn $

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

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

99 _ -> return ()

100

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

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

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

178 return v

179

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

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

181−receiveInput e =

181+receiveInput h e =

182 do i <- getIState

183− l <- runIO $ getLine

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 ""

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

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

185 Left err -> ierror err

190 Left err -> ierror err

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

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

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

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

188− case sexpToCommand sexp of

193+ case IdeSlave.sexpToCommand sexp of

189− Just (REPLCompletions prefix) ->

194+ Just (IdeSlave.REPLCompletions prefix) ->

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

195 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)]

192 ideslavePutSExp "return" good

197 ideslavePutSExp "return" good

193− receiveInput e

198+ receiveInput h e

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

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

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

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

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

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

197 _ -> return Nothing

202 _ -> return Nothing

198

203

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

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

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

203 when d $ dumpState i (proof e)

208 when d $ dumpState i (proof e)

204 (x, h') <-

209 (x, h') <-

205 case idris_outputmode i of

210 case idris_outputmode i of

211+ RawOutput _ ->

206− RawOutput -> runInputT (proverSettings e) $

212+ runInputT (proverSettings e) $

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

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

208− do _ <- case h of

214+ do case h of

209− Just history -> putHistory history

215+ Just history -> putHistory history

210− Nothing -> return ()

216+ Nothing -> return ()

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

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

212− h' <- getHistory

218+ h' <- getHistory

213− return (l, Just h')

219+ return (l, Just h')

214− IdeSlave n ->

220+ IdeSlave _ handle ->

215 do isetPrompt prompt

221 do isetPrompt prompt

216− i <- receiveInput e

222+ i <- receiveInput handle e

217 return (i, h)

223 return (i, h)

218 (cmd, step) <- case x of

224 (cmd, step) <- case x of

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

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

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

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

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

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

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

247 case res of

253 case res of

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

254+ Left err -> do ist <- getIState

255+ iRenderError $ pprintErr ist err

249 ploop fn d prompt prf' st h'

256 ploop fn d prompt prf' st h'

250 Right ok ->

257 Right ok ->

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

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

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

258 ist <- getIState

265 ist <- getIState

259 imp <- impShow

266 imp <- impShow

260 idrisCatch (do

267 idrisCatch (do

261− let h = idris_outh ist

262− OK env = envAtFocus (proof e)

268+ let OK env = envAtFocus (proof e)

263 ctxt' = envCtxt env ctxt

269 ctxt' = envCtxt env ctxt

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

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

265 ist' = ist { tt_ctxt = ctxt' }

271 ist' = ist { tt_ctxt = ctxt' }

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

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

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

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

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

269 let action = case lookupNames n ctxt' of

275 let action = case lookupNames n ctxt' of

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

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

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

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

272 putIState ist

278 putIState ist

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

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

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

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

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

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

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

284 let ppo = ppOptionIst ist

290 let ppo = ppOptionIst ist

285 ty' = normaliseC ctxt [] ty

291 ty' = normaliseC ctxt [] ty

286− h = idris_outh ist

287 infixes = idris_infixes ist

292 infixes = idris_infixes ist

288 action = case tm of

293 action = case tm of

289 TType _ ->

294 TType _ ->

290− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

295+ iPrintTermWithType (prettyImp ppo PType) type1Doc

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

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

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

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

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

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

294 putIState ist

299 putIState ist

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

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

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

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

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

311 infixes = idris_infixes ist

316 infixes = idris_infixes ist

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

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

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

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

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

319+ action = iPrintTermWithType tmDoc tyDoc

315 putIState ist

320 putIState ist

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

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

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

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

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

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

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

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

320− let h = idris_outh ist

321 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

325 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

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

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

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

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

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

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

325 return (False, e, False, prf,

329 return (False, e, False, prf,

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

330+ Right $ iRenderResult (vsep toShow)))

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

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

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

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

329 return $ pprintDocs ist doc

333 return $ pprintDocs ist doc

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

334 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))

335+ return (False, e, False, prf, Right . iRenderResult $ 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)

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

42import Version_idris (gitHash)

43import Util.System

44import Util.DynamicLinker

45−import Util.Net (listenOnLocalhost)

45+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

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

48import Idris.Core.Evaluate

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

91import Data.Either (partitionEithers)

92import Control.DeepSeq

94+import Numeric ( readHex )

95+

94import Debug.Trace

96import Debug.Trace

96-- | Run the REPL

98-- | Run the REPL

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

149 -- TODO: option for port number

151 -- TODO: option for port number

150 serverLoop = withSocketsDo $

152 serverLoop = withSocketsDo $

151 do sock <- listenOnLocalhost $ PortNumber 4294

153 do sock <- listenOnLocalhost $ PortNumber 4294

152− loop fn orig sock

154+ loop fn orig { idris_colourRepl = False } sock

153

155

154 fn = case fn_in of

156 fn = case fn_in of

155 (f:_) -> f

157 (f:_) -> f

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

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

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

160 hSetEncoding h utf8

162 hSetEncoding h utf8

161 cmd <- hGetLine h

163 cmd <- hGetLine h

164+ let isth = case idris_outputmode ist of

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

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

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

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

163 hClose h

168 hClose h

164 loop fn ist' sock

169 loop fn ist' sock

165

170

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

185 setOutH h

190 setOutH h

186 setQuiet True

191 setQuiet True

187 setVerbose False

192 setVerbose False

188− mods <- loadInputs h [f] toline

193+ mods <- loadInputs [f] toline

189 ist <- getIState

194 ist <- getIState

190 return (ist, f)

195 return (ist, f)

191− processNet fn c = do process h fn c

196+ processNet fn c = do process fn c

192 ist <- getIState

197 ist <- getIState

193 return (ist, fn)

198 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}

194

205

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

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

196runClient :: String -> IO ()

207runClient :: String -> IO ()

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

206 else do l <- hGetLine h

217 else do l <- hGetLine h

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

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

208

219

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+

209-- | Run the IdeSlave

228-- | Run the IdeSlave

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

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

211−ideslaveStart orig mods

230+ideslaveStart s orig mods

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

232+ setIdeSlave True h

212− = do i <- getIState

233+ i <- getIState

213 case idris_outputmode i of

234 case idris_outputmode i of

214− IdeSlave n ->

235+ IdeSlave n h ->

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

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 ()

216− ideslave orig mods

240+ ideslave h orig mods

217−

241+

218−

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

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

220−ideslave orig mods

243+ideslave h orig mods

221 = do idrisCatch

244 = 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 ""

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

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

224 Left err -> ierror err

252 Left err -> ierror err

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

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

226 i <- getIState

254 i <- getIState

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

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

228 idrisCatch -- to report correct id back!

256 idrisCatch -- to report correct id back!

229 (do let fn = case mods of

257 (do let fn = case mods of

230 (f:_) -> f

258 (f:_) -> f

231− _ -> ""

259+ _ -> ""

232 case IdeSlave.sexpToCommand sexp of

260 case IdeSlave.sexpToCommand sexp of

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

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

234 Nothing -> iPrintError "did not understand" )

262 Nothing -> iPrintError "did not understand" )

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

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

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

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

237− ideslave orig mods

265+ ideslave h orig mods

238

266

239-- | Run IDESlave commands

267-- | Run IDESlave commands

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

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

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

241 -> IState -- ^^ The original IState

270 -> IState -- ^^ The original IState

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

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

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

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

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

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

245 -> Idris ()

274 -> Idris ()

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

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

247 do c <- colourise

276 do c <- colourise

248 i <- getIState

277 i <- getIState

249 case parseCmd i "(input)" cmd of

278 case parseCmd i "(input)" cmd of

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

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

251 Success (Prove n') ->

280 Success (Prove n') ->

252 idrisCatch

281 idrisCatch

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

282+ (do process fn (Prove n')

254 isetPrompt (mkPrompt mods)

283 isetPrompt (mkPrompt mods)

255 case idris_outputmode i of

284 case idris_outputmode i of

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

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

257− runIO . hPutStrLn stdout $

286+ runIO . hPutStrLn h $

258 IdeSlave.convSExp "return"

287 IdeSlave.convSExp "return"

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

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

260 n

289 n

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

262 (\e -> do ist <- getIState

291 (\e -> do ist <- getIState

263 isetPrompt (mkPrompt mods)

292 isetPrompt (mkPrompt mods)

264 case idris_outputmode i of

293 case idris_outputmode i of

265− IdeSlave n ->

294+ IdeSlave n h ->

266− runIO . hPutStrLn stdout $

295+ runIO . hPutStrLn h $

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

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

268 _ -> return ()

297 _ -> return ()

269− ihRenderError stdout $ pprintErr ist e)

298+ iRenderError $ pprintErr ist e)

270 Success cmd -> idrisCatch

299 Success cmd -> idrisCatch

271 (ideslaveProcess fn cmd)

300 (ideslaveProcess fn cmd)

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

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

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

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

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

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

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

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

276 IdeSlave.toSExp (map replacement compls,

305 IdeSlave.toSExp (map replacement compls,

277 reverse unused)]

306 reverse unused)]

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

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

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

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

280 do i <- getIState

309 do i <- getIState

281 clearErr

310 clearErr

282 putIState (orig { idris_options = idris_options i,

311 putIState (orig { idris_options = idris_options i,

283− idris_outputmode = (IdeSlave id) })

312+ idris_outputmode = (IdeSlave id h) })

284− loadInputs stdout [filename] toline

313+ loadInputs [filename] toline

285 isetPrompt (mkPrompt [filename])

314 isetPrompt (mkPrompt [filename])

286 -- Report either success or failure

315 -- Report either success or failure

287 i <- getIState

316 i <- getIState

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

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

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

292 IdeSlave.toSExp fc])

321 IdeSlave.toSExp fc])

293 (idris_parsedSpan i)

322 (idris_parsedSpan i)

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

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

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

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

296− ideslave orig [filename]

325+ ideslave h orig [filename]

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

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

298 case splitName name of

327 case splitName name of

299 Left err -> iPrintError err

328 Left err -> iPrintError err

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

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

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

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

302 where splitName :: String -> Either String Name

331 where splitName :: String -> Either String Name

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

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

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

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

305 [n] -> Right $ sUN n

334 [n] -> Right $ sUN n

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

335 (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) =

308 case parseConst orig name of

337 case parseConst orig name of

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

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

310 Failure _ ->

339 Failure _ ->

311 case splitName name of

340 case splitName name of

312 Left err -> iPrintError err

341 Left err -> iPrintError err

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

327 case splitName name of

356 case splitName name of

328 Left err -> iPrintError err

357 Left err -> iPrintError err

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

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

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

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

331− process stdout fn (Apropos a)

360+ process fn (Apropos a)

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

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

333 do ist <- getIState

362 do ist <- getIState

334 let opts = idris_options ist

363 let opts = idris_options ist

335 let impshow = opt_showimp opts

364 let impshow = opt_showimp opts

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

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

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

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

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

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

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

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

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

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

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

342 do setImpShow b

371 do setImpShow b

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

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

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

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

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

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

346 do setErrContext b

375 do setErrContext b

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

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

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

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

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

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

350 do ist <- getIState

379 do ist <- getIState

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

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

352 let ppo = ppOptionIst ist

381 let ppo = ppOptionIst ist

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

362 (zip bnds hs),

391 (zip bnds hs),

363 render ist bnd c pc))

392 render ist bnd c pc))

364 splitMvs

393 splitMvs

365− runIO . putStrLn $

394+ runIO . hPutStrLn h $

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

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

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

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

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

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

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

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

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

408 (show n , out, spans)

437 (show n , out, spans)

409

438

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

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

411 case splitName n of

440 case splitName n of

412 Left err -> iPrintError err

441 Left err -> iPrintError err

413 Right n -> do calls <- whoCalls n

442 Right n -> do calls <- whoCalls n

414 ist <- getIState

443 ist <- getIState

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

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

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

445 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

418 where pn ist = displaySpans .

447 where pn ist = displaySpans .

419 renderPretty 0.9 1000 .

448 renderPretty 0.9 1000 .

420 fmap (fancifyAnnots ist) .

449 fmap (fancifyAnnots ist) .

421 prettyName True True []

450 prettyName True True []

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

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

423 case splitName n of

452 case splitName n of

424 Left err -> iPrintError err

453 Left err -> iPrintError err

425 Right n -> do calls <- callsWho n

454 Right n -> do calls <- callsWho n

426 ist <- getIState

455 ist <- getIState

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

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

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

457 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

430 where pn ist = displaySpans .

459 where pn ist = displaySpans .

431 renderPretty 0.9 1000 .

460 renderPretty 0.9 1000 .

432 fmap (fancifyAnnots ist) .

461 fmap (fancifyAnnots ist) .

433 prettyName True True []

462 prettyName True True []

434

463

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

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

436 do ctxt <- getContext

465 do ctxt <- getContext

437 ist <- getIState

466 ist <- getIState

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

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

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

446 displaySpans .

475 displaySpans .

447 renderPretty 0.9 80 .

476 renderPretty 0.9 80 .

448 fmap (fancifyAnnots ist) $ ptm)

477 fmap (fancifyAnnots ist) $ ptm)

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

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

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

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

451− ideSlaveForceTermImplicits id bnd True tm

480+ ideSlaveForceTermImplicits h id bnd True tm

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

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

453− ideSlaveForceTermImplicits id bnd False tm

482+ ideSlaveForceTermImplicits h id bnd False tm

454

483

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

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

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

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

457−ideSlaveForceTermImplicits id bnd impl tm =

486+ideSlaveForceTermImplicits h id bnd impl tm =

458 do ist <- getIState

487 do ist <- getIState

459 let expl = annotate (AnnTerm bnd tm)

488 let expl = annotate (AnnTerm bnd tm)

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

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

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

464 displaySpans .

493 displaySpans .

465 renderPretty 0.9 80 .

494 renderPretty 0.9 80 .

466 fmap (fancifyAnnots ist) $ expl)

495 fmap (fancifyAnnots ist) $ expl)

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

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

468

497

469splitName :: String -> Either String Name

498splitName :: String -> Either String Name

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

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

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

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

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

474

503

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

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

476−ideslaveProcess fn Warranty = process stdout fn Warranty

505+ideslaveProcess fn Warranty = process fn Warranty

477−ideslaveProcess fn Help = process stdout fn Help

506+ideslaveProcess fn Help = process fn Help

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

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

479 iPrintResult "changed directory to"

508 iPrintResult "changed directory to"

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

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

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

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

482 iPrintResult "defined"

511 iPrintResult "defined"

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

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

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

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

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

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

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

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

487−ideslaveProcess fn Universes = process stdout fn Universes

516+ideslaveProcess fn Universes = process fn Universes

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

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

489 iPrintResult ""

518 iPrintResult ""

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

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

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

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

492 iPrintResult ""

521 iPrintResult ""

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

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

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

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

495-- RmProof and AddProof not supported!

524-- RmProof and AddProof not supported!

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

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

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

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

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

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

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

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

500

529

501−ideslaveProcess fn Execute = do process stdout fn Execute

530+ideslaveProcess fn Execute = do process fn Execute

502 iPrintResult ""

531 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)

504 iPrintResult ""

533 iPrintResult ""

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

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

506 iPrintResult ""

535 iPrintResult ""

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

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

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

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

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

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

510 iPrintResult ""

539 iPrintResult ""

511−ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic

540+ideslaveProcess fn ListDynamic = do process fn ListDynamic

512 iPrintResult ""

541 iPrintResult ""

513−ideslaveProcess fn Metavars = process stdout fn Metavars

542+ideslaveProcess fn Metavars = process fn Metavars

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

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

515 iPrintResult ""

544 iPrintResult ""

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

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

517 iPrintResult ""

546 iPrintResult ""

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

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

519 iPrintResult ""

548 iPrintResult ""

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

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

521 iPrintResult ""

550 iPrintResult ""

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

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

523 iPrintResult ""

552 iPrintResult ""

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

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

525 iPrintResult ""

554 iPrintResult ""

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

535 iPrintResult ""

564 iPrintResult ""

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

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

537 iPrintResult ""

566 iPrintResult ""

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

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

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

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

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

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

541

570

542

571

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

568 , idris_colourTheme = idris_colourTheme i

597 , idris_colourTheme = idris_colourTheme i

569 }

598 }

570 clearErr

599 clearErr

571− mods <- loadInputs stdout inputs Nothing

600+ mods <- loadInputs inputs Nothing

572 return (Just inputs)

601 return (Just inputs)

573 Success (Load f toline) ->

602 Success (Load f toline) ->

574 do putIState orig { idris_options = idris_options i

603 do putIState orig { idris_options = idris_options i

575 , idris_colourTheme = idris_colourTheme i

604 , idris_colourTheme = idris_colourTheme i

576 }

605 }

577 clearErr

606 clearErr

578− mod <- loadInputs stdout [f] toline

607+ mod <- loadInputs [f] toline

579 return (Just [f])

608 return (Just [f])

580 Success (ModImport f) ->

609 Success (ModImport f) ->

581 do clearErr

610 do clearErr

582− fmod <- loadModule stdout f

611+ fmod <- loadModule f

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

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

584 Success Edit -> do -- takeMVar stvar

613 Success Edit -> do -- takeMVar stvar

585 edit fn orig

614 edit fn orig

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

588 return (Just inputs)

617 return (Just inputs)

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

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

590 return Nothing

619 return Nothing

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

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

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

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

593 return (Just inputs)

622 return (Just inputs)

594

623

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

624 putIState $ orig { idris_options = idris_options i

653 putIState $ orig { idris_options = idris_options i

625 , idris_colourTheme = idris_colourTheme i

654 , idris_colourTheme = idris_colourTheme i

626 }

655 }

627− loadInputs stdout [f] Nothing

656+ loadInputs [f] Nothing

628-- clearOrigPats

657-- clearOrigPats

629 iucheck

658 iucheck

630 return ()

659 return ()

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

650 = p : "" : prf : xs

679 = p : "" : prf : xs

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

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

652

681

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

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

654−process h fn Help = iPrintResult displayHelp

683+process fn Help = iPrintResult displayHelp

655−process h fn Warranty = iPrintResult warranty

684+process fn Warranty = iPrintResult warranty

656−process h fn (ChangeDirectory f)

685+process fn (ChangeDirectory f)

657 = do runIO $ setCurrentDirectory f

686 = do runIO $ setCurrentDirectory f

658 return ()

687 return ()

659−process h fn (Eval t)

688+process fn (Eval t)

660 = withErrorReflection $ do logLvl 5 $ show t

689 = withErrorReflection $ do logLvl 5 $ show t

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

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

662 ctxt <- getContext

691 ctxt <- getContext

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

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

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

670 let tmDoc = pprintDelab ist tm'

699 let tmDoc = pprintDelab ist tm'

671 tyDoc = pprintDelab ist ty'

700 tyDoc = pprintDelab ist ty'

672− ihPrintTermWithType h tmDoc tyDoc

701+ iPrintTermWithType tmDoc tyDoc

673

702

674

703

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

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

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

677 getName :: PDecl -> Maybe Name

706 getName :: PDecl -> Maybe Name

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

707 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: " ++

703 getRHS (PClauseR fc with rhs whereBlock) = rhs

732 getRHS (PClauseR fc with rhs whereBlock) = rhs

704 getRHS (PWithR fc with rhs whereBlock) = rhs

733 getRHS (PWithR fc with rhs whereBlock) = rhs

705

734

706−process h fn (ExecVal t)

735+process fn (ExecVal t)

707 = do ctxt <- getContext

736 = do ctxt <- getContext

708 ist <- getIState

737 ist <- getIState

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

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

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

712 res <- execute tm

741 res <- execute tm

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

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

714 prettyIst ist (delab ist ty'))

743 prettyIst ist (delab ist ty'))

715− ihPrintTermWithType h resOut tyOut

744+ iPrintTermWithType resOut tyOut

716

745

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

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

718 = do ctxt <- getContext

747 = do ctxt <- getContext

719 ist <- getIState

748 ist <- getIState

720 let ppo = ppOptionIst ist

749 let ppo = ppOptionIst ist

721 case lookupNames n ctxt of

750 case lookupNames n ctxt of

722 ts@(t:_) ->

751 ts@(t:_) ->

723 case lookup t (idris_metavars ist) of

752 case lookup t (idris_metavars ist) of

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

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

725 showMetavarInfo ppo ist n i

754 showMetavarInfo ppo ist n i

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

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

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

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

728 where

757 where

729 showMetavarInfo ppo ist n i

758 showMetavarInfo ppo ist n i

730 = case lookupTy n (tt_ctxt ist) of

759 = case lookupTy n (tt_ctxt ist) of

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

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

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

750

779

751

780

752−process h fn (Check t)

781+process fn (Check t)

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

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

754 ctxt <- getContext

783 ctxt <- getContext

755 ist <- getIState

784 ist <- getIState

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

757 ty' = normaliseC ctxt [] ty

786 ty' = normaliseC ctxt [] ty

758 case tm of

787 case tm of

759 TType _ ->

788 TType _ ->

760− ihPrintTermWithType h (prettyIst ist PType) type1Doc

789+ iPrintTermWithType (prettyIst ist PType) type1Doc

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

790+ _ -> iPrintTermWithType (pprintDelab ist tm)

762− (pprintDelab ist ty)

791+ (pprintDelab ist ty)

763

792

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

793+process fn (DocStr (Left n))

765 = do ist <- getIState

794 = do ist <- getIState

766 case lookupCtxtName n (idris_docstrings ist) of

795 case lookupCtxtName n (idris_docstrings ist) of

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

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

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

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

769− ihRenderResult h (vsep toShow)

798+ iRenderResult (vsep toShow)

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

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

771 return $ pprintDocs ist doc

800 return $ pprintDocs ist doc

772

801

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

802+process fn (DocStr (Right c))

774 = do ist <- getIState

803 = do ist <- getIState

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

804+ iRenderResult $ pprintConstDocs ist c (constDocs c)

776

805

777−process h fn Universes

806+process fn Universes

778 = do i <- getIState

807 = do i <- getIState

779 let cs = idris_constraints i

808 let cs = idris_constraints i

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

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

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

784 case ucheck cs of

813 case ucheck cs of

785 Error e -> iPrintError $ pshow i e

814 Error e -> iPrintError $ pshow i e

786 OK _ -> iPrintResult "Universes OK"

815 OK _ -> iPrintResult "Universes OK"

787−process h fn (Defn n)

816+process fn (Defn n)

788 = do i <- getIState

817 = do i <- getIState

789 iputStrLn "Compiled patterns:\n"

818 iputStrLn "Compiled patterns:\n"

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

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

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

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

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

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

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

801 showTm i' (delab i rhs))

830 showTm i' (delab i rhs))

802−process h fn (TotCheck n)

831+process fn (TotCheck n)

803 = do i <- getIState

832 = do i <- getIState

804 case lookupNameTotal n (tt_ctxt i) of

833 case lookupNameTotal n (tt_ctxt i) of

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

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

806 ts -> do ist <- getIState

835 ts -> do ist <- getIState

807 c <- colourise

836 c <- colourise

808 let ppo = ppOptionIst ist

837 let ppo = ppOptionIst ist

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

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

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

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

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

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

812 ts

841 ts

813

842

814

843

815−process h fn (DebugInfo n)

844+process fn (DebugInfo n)

816 = do i <- getIState

845 = do i <- getIState

817 let oi = lookupCtxtName n (idris_optimisation i)

846 let oi = lookupCtxtName n (idris_optimisation i)

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

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

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

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

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

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

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

831 iputStrLn (show cg')

860 iputStrLn (show cg')

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

861+process fn (Search t) = searchByType t

833−process h fn (CaseSplitAt updatefile l n)

862+process fn (CaseSplitAt updatefile l n)

834− = caseSplitAt h fn updatefile l n

863+ = caseSplitAt fn updatefile l n

835−process h fn (AddClauseFrom updatefile l n)

864+process fn (AddClauseFrom updatefile l n)

836− = addClauseFrom h fn updatefile l n

865+ = addClauseFrom fn updatefile l n

837−process h fn (AddProofClauseFrom updatefile l n)

866+process fn (AddProofClauseFrom updatefile l n)

838− = addProofClauseFrom h fn updatefile l n

867+ = addProofClauseFrom fn updatefile l n

839−process h fn (AddMissing updatefile l n)

868+process fn (AddMissing updatefile l n)

840− = addMissing h fn updatefile l n

869+ = addMissing fn updatefile l n

841−process h fn (MakeWith updatefile l n)

870+process fn (MakeWith updatefile l n)

842− = makeWith h fn updatefile l n

871+ = makeWith fn updatefile l n

843−process h fn (MakeLemma updatefile l n)

872+process fn (MakeLemma updatefile l n)

844− = makeLemma h fn updatefile l n

873+ = makeLemma fn updatefile l n

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

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

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

875+ = doProofSearch fn updatefile rec l n hints Nothing

847−process h fn (Spec t)

876+process fn (Spec t)

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

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

849 ctxt <- getContext

878 ctxt <- getContext

850 ist <- getIState

879 ist <- getIState

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

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

852 iPrintResult (show (delab ist tm'))

881 iPrintResult (show (delab ist tm'))

853

882

854−process h fn (RmProof n')

883+process fn (RmProof n')

855 = do i <- getIState

884 = do i <- getIState

856 n <- resolveProof n'

885 n <- resolveProof n'

857 let proofs = proof_list i

886 let proofs = proof_list i

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

867 let ms = idris_metavars i

896 let ms = idris_metavars i

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

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

869

898

870−process h fn' (AddProof prf)

899+process fn' (AddProof prf)

871 = do fn <- do

900 = do fn <- do

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

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

873 ex <- runIO $ doesFileExist fn''

902 ex <- runIO $ doesFileExist fn''

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

897 iputStrLn $ "Added proof " ++ show n

926 iputStrLn $ "Added proof " ++ show n

898 where ls = (lines prog)

927 where ls = (lines prog)

899

928

900−process h fn (ShowProof n')

929+process fn (ShowProof n')

901 = do i <- getIState

930 = do i <- getIState

902 n <- resolveProof n'

931 n <- resolveProof n'

903 let proofs = proof_list i

932 let proofs = proof_list i

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

905 Nothing -> iPrintError "No proof to show"

934 Nothing -> iPrintError "No proof to show"

906 Just p -> iPrintResult $ showProof False n p

935 Just p -> iPrintResult $ showProof False n p

907

936

908−process h fn (Prove n')

937+process fn (Prove n')

909 = do ctxt <- getContext

938 = do ctxt <- getContext

910 ist <- getIState

939 ist <- getIState

911 let ns = lookupNames n' ctxt

940 let ns = lookupNames n' ctxt

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

923 mapM_ checkDeclTotality (idris_totcheck i)

952 mapM_ checkDeclTotality (idris_totcheck i)

924 warnTotality

953 warnTotality

925

954

926−process h fn (HNF t)

955+process fn (HNF t)

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

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

928 ctxt <- getContext

957 ctxt <- getContext

929 ist <- getIState

958 ist <- getIState

930 let tm' = hnf ctxt [] tm

959 let tm' = hnf ctxt [] tm

931 iPrintResult (show (delab ist tm'))

960 iPrintResult (show (delab ist tm'))

932−process h fn (TestInline t)

961+process fn (TestInline t)

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

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

934 ctxt <- getContext

963 ctxt <- getContext

935 ist <- getIState

964 ist <- getIState

936 let tm' = inlineTerm ist tm

965 let tm' = inlineTerm ist tm

937 c <- colourise

966 c <- colourise

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

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

939−process h fn Execute

968+process fn Execute

940 = idrisCatch

969 = idrisCatch

941 (do ist <- getIState

970 (do ist <- getIState

942 (m, _) <- elabVal recinfo ERHS

971 (m, _) <- elabVal recinfo ERHS

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

948 t <- codegen

977 t <- codegen

949 compile t tmpn m

978 compile t tmpn m

950 case idris_outputmode ist of

979 case idris_outputmode ist of

951− RawOutput -> do runIO $ system tmpn

980+ RawOutput h -> do runIO $ system tmpn

952− return ()

981+ return ()

953− IdeSlave n -> runIO . hPutStrLn h $

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

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

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

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

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

956 where fc = fileFC "main"

985 where fc = fileFC "main"

957−process h fn (Compile codegen f)

986+process fn (Compile codegen f)

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

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

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

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

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

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

961 compile codegen f m

990 compile codegen f m

962 where fc = fileFC "main"

991 where fc = fileFC "main"

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

992+process fn (LogLvl i) = setLogLevel i

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

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

965−process h fn (Pattelab t)

994+process fn (Pattelab t)

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

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

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

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

968

997

969−process h fn (Missing n)

998+process fn (Missing n)

970 = do i <- getIState

999 = do i <- getIState

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

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

972 case lookupCtxt n (idris_patdefs i) of

1001 case lookupCtxt n (idris_patdefs i) of

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

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

974 [(_, tms)] ->

1003 [(_, tms)] ->

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

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

976 _ -> iPrintError $ "Ambiguous name"

1005 _ -> iPrintError $ "Ambiguous name"

977−process h fn (DynamicLink l)

1006+process fn (DynamicLink l)

978 = do i <- getIState

1007 = do i <- getIState

979 let importdirs = opt_importdirs (idris_options i)

1008 let importdirs = opt_importdirs (idris_options i)

980 lib = trim l

1009 lib = trim l

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

987 return ()

1016 return ()

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

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

989 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1018 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

990−process h fn ListDynamic

1019+process fn ListDynamic

991 = do i <- getIState

1020 = do i <- getIState

992 iputStrLn "Dynamic libraries:"

1021 iputStrLn "Dynamic libraries:"

993 showLibs $ idris_dynamic_libs i

1022 showLibs $ idris_dynamic_libs i

994 where showLibs [] = return ()

1023 where showLibs [] = return ()

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

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

996−process h fn Metavars

1025+process fn Metavars

997 = do ist <- getIState

1026 = do ist <- getIState

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

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

999 case mvs of

1028 case mvs of

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

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

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

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

1002−process h fn NOP = return ()

1031+process fn NOP = return ()

1003−

1032+

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

1033+process fn (SetOpt ErrContext) = setErrContext True

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

1034+process fn (UnsetOpt ErrContext) = setErrContext False

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

1035+process fn (SetOpt ShowImpl) = setImpShow True

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

1036+process fn (UnsetOpt ShowImpl) = setImpShow False

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

1037+process fn (SetOpt ShowOrigErr) = setShowOrigErr True

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

1038+process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

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

1039+process fn (SetOpt AutoSolve) = setAutoSolve True

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

1040+process fn (UnsetOpt AutoSolve) = setAutoSolve False

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

1041+process fn (SetOpt NoBanner) = setNoBanner True

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

1042+process fn (UnsetOpt NoBanner) = setNoBanner False

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

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

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

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

1016−

1045+

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

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

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

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

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

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

1020−process h fn ColourOn

1049+process fn ColourOn

1021 = do ist <- getIState

1050 = do ist <- getIState

1022 putIState $ ist { idris_colourRepl = True }

1051 putIState $ ist { idris_colourRepl = True }

1023−process h fn ColourOff

1052+process fn ColourOff

1024 = do ist <- getIState

1053 = do ist <- getIState

1025 putIState $ ist { idris_colourRepl = False }

1054 putIState $ ist { idris_colourRepl = False }

1026−process h fn ListErrorHandlers =

1055+process fn ListErrorHandlers =

1027 do ist <- getIState

1056 do ist <- getIState

1028 iPrintResult $ case idris_errorhandlers ist of

1057 iPrintResult $ case idris_errorhandlers ist of

1029 [] -> "No registered error handlers"

1058 [] -> "No registered error handlers"

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

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

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

1060+process fn (SetConsoleWidth w) = setWidth w

1032

1061

1033−process h fn (Apropos a) =

1062+process fn (Apropos a) =

1034 do ist <- getIState

1063 do ist <- getIState

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

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

1036 let aproposInfo = [ (n,

1065 let aproposInfo = [ (n,

1037 delabTy ist n,

1066 delabTy ist n,

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

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

1039 | n <- sort names, isUN n ]

1068 | n <- sort names, isUN n ]

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

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

1041 where isUN (UN _) = True

1070 where isUN (UN _) = True

1042 isUN (NS n _) = isUN n

1071 isUN (NS n _) = isUN n

1043 isUN _ = False

1072 isUN _ = False

1044

1073

1045−process h fn (WhoCalls n) =

1074+process fn (WhoCalls n) =

1046 do calls <- whoCalls n

1075 do calls <- whoCalls n

1047 ist <- getIState

1076 ist <- getIState

1048− ihRenderResult h . vsep $

1077+ iRenderResult . vsep $

1049 map (\(n, ns) ->

1078 map (\(n, ns) ->

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

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

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

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

1052 calls

1081 calls

1053

1082

1054−process h fn (CallsWho n) =

1083+process fn (CallsWho n) =

1055 do calls <- callsWho n

1084 do calls <- callsWho n

1056 ist <- getIState

1085 ist <- getIState

1057− ihRenderResult h . vsep $

1086+ iRenderResult . vsep $

1058 map (\(n, ns) ->

1087 map (\(n, ns) ->

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

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

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

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

1061 calls

1090 calls

1062-- IdrisDoc

1091-- IdrisDoc

1063−process h fn (MakeDoc s) =

1092+process fn (MakeDoc s) =

1064 do istate <- getIState

1093 do istate <- getIState

1065 let names = words s

1094 let names = words s

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

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

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

1117 [] -> return ()

1146 [] -> return ()

1118

1147

1119

1148

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

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

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

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

1122 = idrisCatch

1151 = idrisCatch

1123 (do ist <- getIState

1152 (do ist <- getIState

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

1153 -- 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

1170 (\e -> do i <- getIState

1199 (\e -> do i <- getIState

1171 case e of

1200 case e of

1172 At f e' -> do setErrSpan f

1201 At f e' -> do setErrSpan f

1173− ihWarn stdout f $ pprintErr i e'

1202+ iWarn f $ pprintErr i e'

1174 ProgramLineComment -> return () -- fail elsewhere

1203 ProgramLineComment -> return () -- fail elsewhere

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

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

1176− ihWarn stdout emptyFC $ pprintErr i e)

1205+ iWarn emptyFC $ pprintErr i e)

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

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

1178 tryLoad :: Bool -> [IFileType] -> Idris ()

1207 tryLoad :: Bool -> [IFileType] -> Idris ()

1179 tryLoad keepstate [] = warnTotality >> return ()

1208 tryLoad keepstate [] = warnTotality >> return ()

@@ -1190,7 +1219,7 @@ loadInputs h inputs toline -- furthest line to read in input source files

1190 then Just l

1219 then Just l

1191 else Nothing

1220 else Nothing

1192 _ -> Nothing

1221 _ -> Nothing

1193− loadFromIFile h f maxline

1222+ loadFromIFile f maxline

1194 inew <- getIState

1223 inew <- getIState

1195 -- FIXME: Save these in IBC to avoid this hack! Need to

1224 -- FIXME: Save these in IBC to avoid this hack! Need to

1196 -- preserve it all from source inputs

1225 -- preserve it all from source inputs

@@ -1238,7 +1267,7 @@ idrisMain opts =

1238 do let inputs = opt getFile opts

1267 do let inputs = opt getFile opts

1239 let quiet = Quiet `elem` opts

1268 let quiet = Quiet `elem` opts

1240 let nobanner = NoBanner `elem` opts

1269 let nobanner = NoBanner `elem` opts

1241− let idesl = Ideslave `elem` opts

1270+ let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts

1242 let runrepl = not (NoREPL `elem` opts)

1271 let runrepl = not (NoREPL `elem` opts)

1243 let verbose = runrepl || Verbose `elem` opts

1272 let verbose = runrepl || Verbose `elem` opts

1244 let output = opt getOutput opts

1273 let output = opt getOutput opts

@@ -1275,7 +1304,6 @@ idrisMain opts =

1275 mapM_ addLangExt (opt getLanguageExt opts)

1304 mapM_ addLangExt (opt getLanguageExt opts)

1276 setREPL runrepl

1305 setREPL runrepl

1277 setQuiet (quiet || isJust script || not (null immediate))

1306 setQuiet (quiet || isJust script || not (null immediate))

1278− setIdeSlave idesl

1279 setVerbose verbose

1307 setVerbose verbose

1280 setCmdLine opts

1308 setCmdLine opts

1281 setOutputTy outty

1309 setOutputTy outty

@@ -1301,9 +1329,9 @@ idrisMain opts =

1301 addPkgDir "base"

1329 addPkgDir "base"

1302 mapM_ addPkgDir pkgdirs

1330 mapM_ addPkgDir pkgdirs

1303 elabPrims

1331 elabPrims

1304− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"

1332+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"

1305 return ()

1333 return ()

1306− when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

1334+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

1307 return ()

1335 return ()

1308

1336

1309 when (runrepl && not idesl) initScript

1337 when (runrepl && not idesl) initScript

@@ -1319,14 +1347,14 @@ idrisMain opts =

1319 iputStrLn banner

1347 iputStrLn banner

1320

1348

1321 orig <- getIState

1349 orig <- getIState

1322− loadInputs stdout inputs Nothing

1350+ when (not idesl) $ loadInputs inputs Nothing

1323

1351

1324 runIO $ hSetBuffering stdout LineBuffering

1352 runIO $ hSetBuffering stdout LineBuffering

1325

1353

1326 ok <- noErrors

1354 ok <- noErrors

1327 when ok $ case output of

1355 when ok $ case output of

1328 [] -> return ()

1356 [] -> return ()

1329− (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1357+ (o:_) -> idrisCatch (process "" (Compile cgn o))

1330 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1358 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1331

1359

1332 case immediate of

1360 case immediate of

@@ -1337,7 +1365,7 @@ idrisMain opts =

1337 case parseExpr ist str of

1365 case parseExpr ist str of

1338 Failure err -> do iputStrLn $ show (fixColour c err)

1366 Failure err -> do iputStrLn $ show (fixColour c err)

1339 runIO $ exitWith (ExitFailure 1)

1367 runIO $ exitWith (ExitFailure 1)

1340− Success e -> process stdout "" (Eval e))

1368+ Success e -> process "" (Eval e))

1341 exprs

1369 exprs

1342 runIO $ exitWith ExitSuccess

1370 runIO $ exitWith ExitSuccess

1343

1371

@@ -1359,7 +1387,8 @@ idrisMain opts =

1359-- clearOrigPats

1387-- clearOrigPats

1360 startServer orig inputs

1388 startServer orig inputs

1361 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1389 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1390+ let idesock = IdeslaveSocket `elem` opts

1362− when (idesl) $ ideslaveStart orig inputs

1391+ when (idesl) $ ideslaveStart idesock orig inputs

1363 ok <- noErrors

1392 ok <- noErrors

1364 when (not ok) $ runIO (exitWith (ExitFailure 1))

1393 when (not ok) $ runIO (exitWith (ExitFailure 1))

1365 where

1394 where

@@ -1421,7 +1450,7 @@ initScript = do script <- getInitScript

1421 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

1450 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

1422 Success Proofs -> proofs i

1451 Success Proofs -> proofs i

1423 Success Quit -> iPrintError "Init scripts cannot quit Idris"

1452 Success Quit -> iPrintError "Init scripts cannot quit Idris"

1424− Success cmd -> process stdout [] cmd

1453+ Success cmd -> process [] cmd

1425

1454

1426getFile :: Opt -> Maybe String

1455getFile :: Opt -> Maybe String

1427getFile (Filename str) = Just str

1456getFile (Filename str) = Just str

src/Idris/TypeSearch.hs+6−8

@@ -29,14 +29,12 @@ import Idris.Core.Unify (match_unify)

29import Idris.Delaborate (delabTy)

30import Idris.Docstrings (noDocs, overview)

31import Idris.Elab.Type (elabType)

32−import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)

32+import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)

33−

34−import System.IO (Handle)

36import Util.Pretty (text, char, vsep, (<>), Doc)

34import Util.Pretty (text, char, vsep, (<>), Doc)

38−searchByType :: Handle -> PTerm -> Idris ()

36+searchByType :: PTerm -> Idris ()

39−searchByType h pterm = do

37+searchByType pterm = do

40 pterm' <- addUsingConstraints syn emptyFC pterm

38 pterm' <- addUsingConstraints syn emptyFC pterm

41 pterm'' <- implicit toplevel syn n pterm'

39 pterm'' <- implicit toplevel syn n pterm'

42 i <- getIState

40 i <- getIState

@@ -50,9 +48,9 @@ searchByType h pterm = do

50 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

48 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

51 | (n, score) <- names']

49 | (n, score) <- names']

52 case idris_outputmode i of

50 case idris_outputmode i of

53− RawOutput -> do mapM_ (ihRenderOutput h) docs

51+ RawOutput _ -> do mapM_ iRenderOutput docs

54− ihPrintResult h ""

52+ iPrintResult ""

55− IdeSlave n -> ihRenderResult h (vsep docs)

53+ IdeSlave n h -> iRenderResult (vsep docs)

56 where

54 where

57 numLimit = 50

55 numLimit = 50

58 syn = defaultSyntax { implicitAllowed = True } -- syntax

56 syn = defaultSyntax { implicitAllowed = True } -- syntax

src/Pkg/Package.hs+1−1

@@ -144,7 +144,7 @@ documentPkg fp =

144 setCurrentDirectory $ pkgDir

145 let run l = runErrorT . (execStateT l)

146 load [] = return ()

147− load (f:fs) = do loadModule stdout f; load fs

147+ load (f:fs) = do loadModule f; load fs

148 loader = do idrisMain opts; load fs

149 idrisInstance <- run loader idrisInit

150 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)

4import Network.Socket hiding (sClose, PortNumber)

5import Network.BSD (getProtocolNumber)

6import Control.Exception (bracketOnError)

@@ -20,3 +20,16 @@ listenOnLocalhost (PortNumber port) = do

20 return sock

21 )

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+ )