480024c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove all the handle arguments

480024cDavid Raymond Christiansen12 years ago

src/Idris/AbsSyntax.hs+1−5

compare with master

unifiedsplit

@@ -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,7 +789,7 @@ 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 h ->

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 . hPutStrLn h $ convSExp "log" good n

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

src/Idris/AbsSyntaxTree.hs+5−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 Handle 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

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+1

@@ -247,6 +247,7 @@ sexpToCommand _

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

248parseMessage x = case receiveString x of

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

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

250 Left err -> Left err

251 Left err -> Left err

251

252

252receiveString :: String -> Either Err SExp

253receiveString :: String -> Either Err SExp

src/Idris/Interactive.hs+25−25

@@ -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,7 +266,7 @@ 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 h ->

271 let good = SexpList [SymbolAtom "ok",

272 SexpList [SymbolAtom "metavariable-lemma",

@@ -284,7 +284,7 @@ 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 h ->

289 let good = SexpList [SymbolAtom "ok",

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

src/Idris/Output.hs+52−55

@@ -24,20 +24,21 @@ 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 h ->

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

@@ -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 h ->

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 . hPutStrLn h $ 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 h -> 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,17 +112,17 @@ 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 h -> 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 h ->

128 IdeSlave n h ->

@@ -129,22 +130,18 @@ ihPrintWithStatus status h s = do

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

@@ -156,7 +153,7 @@ ideslavePutSExp cmd info = do i <- getIState

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

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]

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 h -> ihWarn h 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+27−32

@@ -25,9 +25,9 @@ import Idris.TypeSearch (searchByType)

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

28+import System.IO (Handle)

28import System.Console.Haskeline

29import System.Console.Haskeline

29import System.Console.Haskeline.History

30import System.Console.Haskeline.History

30−import System.IO (Handle)

31import Control.Monad.State.Strict

32import Control.DeepSeq

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

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

95 solveDeferred n

96 case idris_outputmode i of

97− IdeSlave n h ->

97+ IdeSlave n _ ->

98− ihputStrLn h $ convSExp "return" (SymbolAtom "ok", "") n

98+ iputStrLn $ convSExp "return" (SymbolAtom "ok", "") n

99 _ -> return ()

100

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

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

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

178 return v

179

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

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

181−receiveInput e handle =

181+receiveInput h e =

182 do i <- getIState

183 l <- runIO $ getLine

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

185 Left err -> ierror err

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

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

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

188 case sexpToCommand sexp of

189 Just (REPLCompletions prefix) ->

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

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

192 ideslavePutSExp "return" good

193− receiveInput e handle

193+ receiveInput h e

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

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

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

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

203 when d $ dumpState i (proof e)

204 (x, h') <-

205 case idris_outputmode i of

206+ RawOutput _ ->

206− RawOutput -> runInputT (proverSettings e) $

207+ runInputT (proverSettings e) $

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

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

208− do _ <- case h of

209+ do case h of

209− Just history -> putHistory history

210+ Just history -> putHistory history

210− Nothing -> return ()

211+ Nothing -> return ()

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

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

212− h' <- getHistory

213+ h' <- getHistory

213− return (l, Just h')

214+ return (l, Just h')

214 IdeSlave _ handle ->

215 IdeSlave _ handle ->

215 do isetPrompt prompt

216 do isetPrompt prompt

216− i <- receiveInput e handle

217+ i <- receiveInput handle e

217 return (i, h)

218 return (i, h)

218 (cmd, step) <- case x of

219 (cmd, step) <- case x of

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

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

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

258 ist <- getIState

259 ist <- getIState

259 imp <- impShow

260 imp <- impShow

260 idrisCatch (do

261 idrisCatch (do

261− let h = idris_outh ist

262− OK env = envAtFocus (proof e)

262+ let OK env = envAtFocus (proof e)

263 ctxt' = envCtxt env ctxt

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

265 ist' = ist { tt_ctxt = ctxt' }

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

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

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

269 let action = case lookupNames n ctxt' of

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

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

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

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

272 putIState ist

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

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

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

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

284 let ppo = ppOptionIst ist

285 ty' = normaliseC ctxt [] ty

286− h = idris_outh ist

287 infixes = idris_infixes ist

286 infixes = idris_infixes ist

288 action = case tm of

287 action = case tm of

289 TType _ ->

288 TType _ ->

290− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

289+ iPrintTermWithType (prettyImp ppo PType) type1Doc

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

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

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

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

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

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

294 putIState ist

293 putIState ist

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

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

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

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

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

311 infixes = idris_infixes ist

310 infixes = idris_infixes ist

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

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

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

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

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

313+ action = iPrintTermWithType tmDoc tyDoc

315 putIState ist

314 putIState ist

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

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

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

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

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

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

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

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

320− let h = idris_outh ist

321 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

319 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

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

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

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

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

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

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

325 return (False, e, False, prf,

323 return (False, e, False, prf,

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

324+ Right $ iRenderResult (vsep toShow)))

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

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

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

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

329 return $ pprintDocs ist doc

327 return $ pprintDocs ist doc

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

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

329+ 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)

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

src/Idris/REPL.hs+175−169

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

187 setOutH h

188 setQuiet True

189 setVerbose False

190− mods <- loadInputs h [f] toline

190+ mods <- loadInputs [f] toline

191 ist <- getIState

192 return (ist, f)

193− processNet fn c = do process h fn c

193+ processNet fn c = do process fn c

194 ist <- getIState

195 return (ist, fn)

196+ setOutH :: Handle -> Idris ()

197+ setOutH h =

198+ do ist <- getIState

199+ case idris_outputmode ist of

200+ RawOutput _ -> putIState ist {idris_outputmode = RawOutput h}

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

196

202

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

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

198runClient :: String -> IO ()

204runClient :: String -> IO ()

@@ -208,7 +214,7 @@ runClient str = withSocketsDo $ do

208 else do l <- hGetLine h

214 else do l <- hGetLine h

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

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

210

216

211−initIdeslaveSocket :: IO (Handle)

217+initIdeslaveSocket :: IO Handle

212initIdeslaveSocket = do

218initIdeslaveSocket = do

213 (sock, port) <- listenOnLocalhostAnyPort

219 (sock, port) <- listenOnLocalhostAnyPort

214 putStrLn $ show port

220 putStrLn $ show port

@@ -276,7 +282,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

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

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

277 Success (Prove n') ->

283 Success (Prove n') ->

278 idrisCatch

284 idrisCatch

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

285+ (do process fn (Prove n')

280 isetPrompt (mkPrompt mods)

286 isetPrompt (mkPrompt mods)

281 case idris_outputmode i of

287 case idris_outputmode i of

282 IdeSlave n h -> -- signal completion of proof to ide

288 IdeSlave n h -> -- signal completion of proof to ide

@@ -292,10 +298,10 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

292 runIO . hPutStrLn h $

298 runIO . hPutStrLn h $

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

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

294 _ -> return ()

300 _ -> return ()

295− ihRenderError h $ pprintErr ist e)

301+ iRenderError $ pprintErr ist e)

296 Success cmd -> idrisCatch

302 Success cmd -> idrisCatch

297 (ideslaveProcess fn cmd)

303 (ideslaveProcess fn cmd)

298− (\e -> getIState >>= ihRenderError h . flip pprintErr e)

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

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

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

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

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

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

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

@@ -307,7 +313,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

307 clearErr

313 clearErr

308 putIState (orig { idris_options = idris_options i,

314 putIState (orig { idris_options = idris_options i,

309 idris_outputmode = (IdeSlave id h) })

315 idris_outputmode = (IdeSlave id h) })

310− loadInputs stdout [filename] toline

316+ loadInputs [filename] toline

311 isetPrompt (mkPrompt [filename])

317 isetPrompt (mkPrompt [filename])

312 -- Report either success or failure

318 -- Report either success or failure

313 i <- getIState

319 i <- getIState

@@ -323,7 +329,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

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

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

324 case splitName name of

330 case splitName name of

325 Left err -> iPrintError err

331 Left err -> iPrintError err

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

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

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

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

328 where splitName :: String -> Either String Name

334 where splitName :: String -> Either String Name

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

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

@@ -332,29 +338,29 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =

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

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

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

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

334 case parseConst orig name of

340 case parseConst orig name of

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

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

336 Failure _ ->

342 Failure _ ->

337 case splitName name of

343 case splitName name of

338 Left err -> iPrintError err

344 Left err -> iPrintError err

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

353 case splitName name of

359 case splitName name of

354 Left err -> iPrintError err

360 Left err -> iPrintError err

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

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

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

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

357− process stdout fn (Apropos a)

363+ process fn (Apropos a)

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

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

359 do ist <- getIState

365 do ist <- getIState

360 let opts = idris_options ist

366 let opts = idris_options ist

@@ -499,70 +505,70 @@ splitName s = case reverse $ splitOn "." s of

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

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

500

506

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

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

502−ideslaveProcess fn Warranty = process stdout fn Warranty

508+ideslaveProcess fn Warranty = process fn Warranty

503−ideslaveProcess fn Help = process stdout fn Help

509+ideslaveProcess fn Help = process fn Help

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

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

505 iPrintResult "changed directory to"

511 iPrintResult "changed directory to"

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

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

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

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

508 iPrintResult "defined"

514 iPrintResult "defined"

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

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

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

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

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

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

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

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

513−ideslaveProcess fn Universes = process stdout fn Universes

519+ideslaveProcess fn Universes = process fn Universes

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

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

515 iPrintResult ""

521 iPrintResult ""

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

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

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

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

518 iPrintResult ""

524 iPrintResult ""

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

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

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

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

521-- RmProof and AddProof not supported!

527-- RmProof and AddProof not supported!

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

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

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

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

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

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

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

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

526

532

527−ideslaveProcess fn Execute = do process stdout fn Execute

533+ideslaveProcess fn Execute = do process fn Execute

528 iPrintResult ""

534 iPrintResult ""

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

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

530 iPrintResult ""

536 iPrintResult ""

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

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

532 iPrintResult ""

538 iPrintResult ""

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

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

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

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

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

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

536 iPrintResult ""

542 iPrintResult ""

537−ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic

543+ideslaveProcess fn ListDynamic = do process fn ListDynamic

538 iPrintResult ""

544 iPrintResult ""

539−ideslaveProcess fn Metavars = process stdout fn Metavars

545+ideslaveProcess fn Metavars = process fn Metavars

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

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

541 iPrintResult ""

547 iPrintResult ""

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

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

543 iPrintResult ""

549 iPrintResult ""

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

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

545 iPrintResult ""

551 iPrintResult ""

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

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

547 iPrintResult ""

553 iPrintResult ""

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

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

549 iPrintResult ""

555 iPrintResult ""

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

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

551 iPrintResult ""

557 iPrintResult ""

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

561 iPrintResult ""

567 iPrintResult ""

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

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

563 iPrintResult ""

569 iPrintResult ""

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

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

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

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

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

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

567

573

568

574

@@ -594,18 +600,18 @@ processInput cmd orig inputs

594 , idris_colourTheme = idris_colourTheme i

600 , idris_colourTheme = idris_colourTheme i

595 }

601 }

596 clearErr

602 clearErr

597− mods <- loadInputs stdout inputs Nothing

603+ mods <- loadInputs inputs Nothing

598 return (Just inputs)

604 return (Just inputs)

599 Success (Load f toline) ->

605 Success (Load f toline) ->

600 do putIState orig { idris_options = idris_options i

606 do putIState orig { idris_options = idris_options i

601 , idris_colourTheme = idris_colourTheme i

607 , idris_colourTheme = idris_colourTheme i

602 }

608 }

603 clearErr

609 clearErr

604− mod <- loadInputs stdout [f] toline

610+ mod <- loadInputs [f] toline

605 return (Just [f])

611 return (Just [f])

606 Success (ModImport f) ->

612 Success (ModImport f) ->

607 do clearErr

613 do clearErr

608− fmod <- loadModule stdout f

614+ fmod <- loadModule f

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

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

610 Success Edit -> do -- takeMVar stvar

616 Success Edit -> do -- takeMVar stvar

611 edit fn orig

617 edit fn orig

@@ -614,7 +620,7 @@ processInput cmd orig inputs

614 return (Just inputs)

620 return (Just inputs)

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

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

616 return Nothing

622 return Nothing

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

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

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

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

619 return (Just inputs)

625 return (Just inputs)

620

626

@@ -650,7 +656,7 @@ edit f orig

650 putIState $ orig { idris_options = idris_options i

656 putIState $ orig { idris_options = idris_options i

651 , idris_colourTheme = idris_colourTheme i

657 , idris_colourTheme = idris_colourTheme i

652 }

658 }

653− loadInputs stdout [f] Nothing

659+ loadInputs [f] Nothing

654-- clearOrigPats

660-- clearOrigPats

655 iucheck

661 iucheck

656 return ()

662 return ()

@@ -676,13 +682,13 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

676 = p : "" : prf : xs

682 = p : "" : prf : xs

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

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

678

684

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

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

680−process h fn Help = iPrintResult displayHelp

686+process fn Help = iPrintResult displayHelp

681−process h fn Warranty = iPrintResult warranty

687+process fn Warranty = iPrintResult warranty

682−process h fn (ChangeDirectory f)

688+process fn (ChangeDirectory f)

683 = do runIO $ setCurrentDirectory f

689 = do runIO $ setCurrentDirectory f

684 return ()

690 return ()

685−process h fn (Eval t)

691+process fn (Eval t)

686 = withErrorReflection $ do logLvl 5 $ show t

692 = withErrorReflection $ do logLvl 5 $ show t

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

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

688 ctxt <- getContext

694 ctxt <- getContext

@@ -695,10 +701,10 @@ process h fn (Eval t)

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

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

696 let tmDoc = pprintDelab ist tm'

702 let tmDoc = pprintDelab ist tm'

697 tyDoc = pprintDelab ist ty'

703 tyDoc = pprintDelab ist ty'

698− ihPrintTermWithType h tmDoc tyDoc

704+ iPrintTermWithType tmDoc tyDoc

699

705

700

706

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

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

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

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

703 getName :: PDecl -> Maybe Name

709 getName :: PDecl -> Maybe Name

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

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

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

729 getRHS (PClauseR fc with rhs whereBlock) = rhs

735 getRHS (PClauseR fc with rhs whereBlock) = rhs

730 getRHS (PWithR fc with rhs whereBlock) = rhs

736 getRHS (PWithR fc with rhs whereBlock) = rhs

731

737

732−process h fn (ExecVal t)

738+process fn (ExecVal t)

733 = do ctxt <- getContext

739 = do ctxt <- getContext

734 ist <- getIState

740 ist <- getIState

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

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

@@ -738,19 +744,19 @@ process h fn (ExecVal t)

738 res <- execute tm

744 res <- execute tm

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

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

740 prettyIst ist (delab ist ty'))

746 prettyIst ist (delab ist ty'))

741− ihPrintTermWithType h resOut tyOut

747+ iPrintTermWithType resOut tyOut

742

748

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

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

744 = do ctxt <- getContext

750 = do ctxt <- getContext

745 ist <- getIState

751 ist <- getIState

746 let ppo = ppOptionIst ist

752 let ppo = ppOptionIst ist

747 case lookupNames n ctxt of

753 case lookupNames n ctxt of

748 ts@(t:_) ->

754 ts@(t:_) ->

749 case lookup t (idris_metavars ist) of

755 case lookup t (idris_metavars ist) of

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

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

751 showMetavarInfo ppo ist n i

757 showMetavarInfo ppo ist n i

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

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

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

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

754 where

760 where

755 showMetavarInfo ppo ist n i

761 showMetavarInfo ppo ist n i

756 = case lookupTy n (tt_ctxt ist) of

762 = case lookupTy n (tt_ctxt ist) of

@@ -775,7 +781,7 @@ process h fn (Check (PRef _ n))

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

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

776

782

777

783

778−process h fn (Check t)

784+process fn (Check t)

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

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

780 ctxt <- getContext

786 ctxt <- getContext

781 ist <- getIState

787 ist <- getIState

@@ -783,24 +789,24 @@ process h fn (Check t)

783 ty' = normaliseC ctxt [] ty

789 ty' = normaliseC ctxt [] ty

784 case tm of

790 case tm of

785 TType _ ->

791 TType _ ->

786− ihPrintTermWithType h (prettyIst ist PType) type1Doc

792+ iPrintTermWithType (prettyIst ist PType) type1Doc

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

793+ _ -> iPrintTermWithType (pprintDelab ist tm)

788− (pprintDelab ist ty)

794+ (pprintDelab ist ty)

789

795

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

796+process fn (DocStr (Left n))

791 = do ist <- getIState

797 = do ist <- getIState

792 case lookupCtxtName n (idris_docstrings ist) of

798 case lookupCtxtName n (idris_docstrings ist) of

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

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

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

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

795− ihRenderResult h (vsep toShow)

801+ iRenderResult (vsep toShow)

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

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

797 return $ pprintDocs ist doc

803 return $ pprintDocs ist doc

798

804

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

805+process fn (DocStr (Right c))

800 = do ist <- getIState

806 = do ist <- getIState

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

807+ iRenderResult $ pprintConstDocs ist c (constDocs c)

802

808

803−process h fn Universes

809+process fn Universes

804 = do i <- getIState

810 = do i <- getIState

805 let cs = idris_constraints i

811 let cs = idris_constraints i

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

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

@@ -810,7 +816,7 @@ process h fn Universes

810 case ucheck cs of

816 case ucheck cs of

811 Error e -> iPrintError $ pshow i e

817 Error e -> iPrintError $ pshow i e

812 OK _ -> iPrintResult "Universes OK"

818 OK _ -> iPrintResult "Universes OK"

813−process h fn (Defn n)

819+process fn (Defn n)

814 = do i <- getIState

820 = do i <- getIState

815 iputStrLn "Compiled patterns:\n"

821 iputStrLn "Compiled patterns:\n"

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

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

@@ -825,20 +831,20 @@ process h fn (Defn n)

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

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

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

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

827 showTm i' (delab i rhs))

833 showTm i' (delab i rhs))

828−process h fn (TotCheck n)

834+process fn (TotCheck n)

829 = do i <- getIState

835 = do i <- getIState

830 case lookupNameTotal n (tt_ctxt i) of

836 case lookupNameTotal n (tt_ctxt i) of

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

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

832 ts -> do ist <- getIState

838 ts -> do ist <- getIState

833 c <- colourise

839 c <- colourise

834 let ppo = ppOptionIst ist

840 let ppo = ppOptionIst ist

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

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

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

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

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

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

838 ts

844 ts

839

845

840

846

841−process h fn (DebugInfo n)

847+process fn (DebugInfo n)

842 = do i <- getIState

848 = do i <- getIState

843 let oi = lookupCtxtName n (idris_optimisation i)

849 let oi = lookupCtxtName n (idris_optimisation i)

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

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

@@ -855,29 +861,29 @@ process h fn (DebugInfo n)

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

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

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

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

857 iputStrLn (show cg')

863 iputStrLn (show cg')

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

864+process fn (Search t) = searchByType t

859−process h fn (CaseSplitAt updatefile l n)

865+process fn (CaseSplitAt updatefile l n)

860− = caseSplitAt h fn updatefile l n

866+ = caseSplitAt fn updatefile l n

861−process h fn (AddClauseFrom updatefile l n)

867+process fn (AddClauseFrom updatefile l n)

862− = addClauseFrom h fn updatefile l n

868+ = addClauseFrom fn updatefile l n

863−process h fn (AddProofClauseFrom updatefile l n)

869+process fn (AddProofClauseFrom updatefile l n)

864− = addProofClauseFrom h fn updatefile l n

870+ = addProofClauseFrom fn updatefile l n

865−process h fn (AddMissing updatefile l n)

871+process fn (AddMissing updatefile l n)

866− = addMissing h fn updatefile l n

872+ = addMissing fn updatefile l n

867−process h fn (MakeWith updatefile l n)

873+process fn (MakeWith updatefile l n)

868− = makeWith h fn updatefile l n

874+ = makeWith fn updatefile l n

869−process h fn (MakeLemma updatefile l n)

875+process fn (MakeLemma updatefile l n)

870− = makeLemma h fn updatefile l n

876+ = makeLemma fn updatefile l n

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

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

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

878+ = doProofSearch fn updatefile rec l n hints Nothing

873−process h fn (Spec t)

879+process fn (Spec t)

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

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

875 ctxt <- getContext

881 ctxt <- getContext

876 ist <- getIState

882 ist <- getIState

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

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

878 iPrintResult (show (delab ist tm'))

884 iPrintResult (show (delab ist tm'))

879

885

880−process h fn (RmProof n')

886+process fn (RmProof n')

881 = do i <- getIState

887 = do i <- getIState

882 n <- resolveProof n'

888 n <- resolveProof n'

883 let proofs = proof_list i

889 let proofs = proof_list i

@@ -893,7 +899,7 @@ process h fn (RmProof n')

893 let ms = idris_metavars i

899 let ms = idris_metavars i

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

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

895

901

896−process h fn' (AddProof prf)

902+process fn' (AddProof prf)

897 = do fn <- do

903 = do fn <- do

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

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

899 ex <- runIO $ doesFileExist fn''

905 ex <- runIO $ doesFileExist fn''

@@ -923,7 +929,7 @@ process h fn' (AddProof prf)

923 iputStrLn $ "Added proof " ++ show n

929 iputStrLn $ "Added proof " ++ show n

924 where ls = (lines prog)

930 where ls = (lines prog)

925

931

926−process h fn (ShowProof n')

932+process fn (ShowProof n')

927 = do i <- getIState

933 = do i <- getIState

928 n <- resolveProof n'

934 n <- resolveProof n'

929 let proofs = proof_list i

935 let proofs = proof_list i

@@ -931,7 +937,7 @@ process h fn (ShowProof n')

931 Nothing -> iPrintError "No proof to show"

937 Nothing -> iPrintError "No proof to show"

932 Just p -> iPrintResult $ showProof False n p

938 Just p -> iPrintResult $ showProof False n p

933

939

934−process h fn (Prove n')

940+process fn (Prove n')

935 = do ctxt <- getContext

941 = do ctxt <- getContext

936 ist <- getIState

942 ist <- getIState

937 let ns = lookupNames n' ctxt

943 let ns = lookupNames n' ctxt

@@ -949,20 +955,20 @@ process h fn (Prove n')

949 mapM_ checkDeclTotality (idris_totcheck i)

955 mapM_ checkDeclTotality (idris_totcheck i)

950 warnTotality

956 warnTotality

951

957

952−process h fn (HNF t)

958+process fn (HNF t)

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

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

954 ctxt <- getContext

960 ctxt <- getContext

955 ist <- getIState

961 ist <- getIState

956 let tm' = hnf ctxt [] tm

962 let tm' = hnf ctxt [] tm

957 iPrintResult (show (delab ist tm'))

963 iPrintResult (show (delab ist tm'))

958−process h fn (TestInline t)

964+process fn (TestInline t)

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

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

960 ctxt <- getContext

966 ctxt <- getContext

961 ist <- getIState

967 ist <- getIState

962 let tm' = inlineTerm ist tm

968 let tm' = inlineTerm ist tm

963 c <- colourise

969 c <- colourise

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

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

965−process h fn Execute

971+process fn Execute

966 = idrisCatch

972 = idrisCatch

967 (do ist <- getIState

973 (do ist <- getIState

968 (m, _) <- elabVal recinfo ERHS

974 (m, _) <- elabVal recinfo ERHS

@@ -974,33 +980,33 @@ process h fn Execute

974 t <- codegen

980 t <- codegen

975 compile t tmpn m

981 compile t tmpn m

976 case idris_outputmode ist of

982 case idris_outputmode ist of

977− RawOutput -> do runIO $ system tmpn

983+ RawOutput h -> do runIO $ system tmpn

978− return ()

984+ return ()

979 IdeSlave n h -> runIO . hPutStrLn h $

985 IdeSlave n h -> runIO . hPutStrLn h $

980 IdeSlave.convSExp "run-program" tmpn n)

986 IdeSlave.convSExp "run-program" tmpn n)

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

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

982 where fc = fileFC "main"

988 where fc = fileFC "main"

983−process h fn (Compile codegen f)

989+process fn (Compile codegen f)

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

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

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

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

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

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

987 compile codegen f m

993 compile codegen f m

988 where fc = fileFC "main"

994 where fc = fileFC "main"

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

995+process fn (LogLvl i) = setLogLevel i

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

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

991−process h fn (Pattelab t)

997+process fn (Pattelab t)

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

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

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

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

994

1000

995−process h fn (Missing n)

1001+process fn (Missing n)

996 = do i <- getIState

1002 = do i <- getIState

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

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

998 case lookupCtxt n (idris_patdefs i) of

1004 case lookupCtxt n (idris_patdefs i) of

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

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

1000 [(_, tms)] ->

1006 [(_, tms)] ->

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

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

1002 _ -> iPrintError $ "Ambiguous name"

1008 _ -> iPrintError $ "Ambiguous name"

1003−process h fn (DynamicLink l)

1009+process fn (DynamicLink l)

1004 = do i <- getIState

1010 = do i <- getIState

1005 let importdirs = opt_importdirs (idris_options i)

1011 let importdirs = opt_importdirs (idris_options i)

1006 lib = trim l

1012 lib = trim l

@@ -1013,80 +1019,80 @@ process h fn (DynamicLink l)

1013 return ()

1019 return ()

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

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

1015 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1021 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1016−process h fn ListDynamic

1022+process fn ListDynamic

1017 = do i <- getIState

1023 = do i <- getIState

1018 iputStrLn "Dynamic libraries:"

1024 iputStrLn "Dynamic libraries:"

1019 showLibs $ idris_dynamic_libs i

1025 showLibs $ idris_dynamic_libs i

1020 where showLibs [] = return ()

1026 where showLibs [] = return ()

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

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

1022−process h fn Metavars

1028+process fn Metavars

1023 = do ist <- getIState

1029 = do ist <- getIState

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

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

1025 case mvs of

1031 case mvs of

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

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

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

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

1028−process h fn NOP = return ()

1034+process fn NOP = return ()

1029−

1035+

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

1036+process fn (SetOpt ErrContext) = setErrContext True

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

1037+process fn (UnsetOpt ErrContext) = setErrContext False

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

1038+process fn (SetOpt ShowImpl) = setImpShow True

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

1039+process fn (UnsetOpt ShowImpl) = setImpShow False

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

1040+process fn (SetOpt ShowOrigErr) = setShowOrigErr True

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

1041+process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

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

1042+process fn (SetOpt AutoSolve) = setAutoSolve True

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

1043+process fn (UnsetOpt AutoSolve) = setAutoSolve False

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

1044+process fn (SetOpt NoBanner) = setNoBanner True

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

1045+process fn (UnsetOpt NoBanner) = setNoBanner False

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

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

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

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

1042−

1048+

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

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

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

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

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

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

1046−process h fn ColourOn

1052+process fn ColourOn

1047 = do ist <- getIState

1053 = do ist <- getIState

1048 putIState $ ist { idris_colourRepl = True }

1054 putIState $ ist { idris_colourRepl = True }

1049−process h fn ColourOff

1055+process fn ColourOff

1050 = do ist <- getIState

1056 = do ist <- getIState

1051 putIState $ ist { idris_colourRepl = False }

1057 putIState $ ist { idris_colourRepl = False }

1052−process h fn ListErrorHandlers =

1058+process fn ListErrorHandlers =

1053 do ist <- getIState

1059 do ist <- getIState

1054 iPrintResult $ case idris_errorhandlers ist of

1060 iPrintResult $ case idris_errorhandlers ist of

1055 [] -> "No registered error handlers"

1061 [] -> "No registered error handlers"

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

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

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

1063+process fn (SetConsoleWidth w) = setWidth w

1058

1064

1059−process h fn (Apropos a) =

1065+process fn (Apropos a) =

1060 do ist <- getIState

1066 do ist <- getIState

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

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

1062 let aproposInfo = [ (n,

1068 let aproposInfo = [ (n,

1063 delabTy ist n,

1069 delabTy ist n,

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

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

1065 | n <- sort names, isUN n ]

1071 | n <- sort names, isUN n ]

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

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

1067 where isUN (UN _) = True

1073 where isUN (UN _) = True

1068 isUN (NS n _) = isUN n

1074 isUN (NS n _) = isUN n

1069 isUN _ = False

1075 isUN _ = False

1070

1076

1071−process h fn (WhoCalls n) =

1077+process fn (WhoCalls n) =

1072 do calls <- whoCalls n

1078 do calls <- whoCalls n

1073 ist <- getIState

1079 ist <- getIState

1074− ihRenderResult h . vsep $

1080+ iRenderResult . vsep $

1075 map (\(n, ns) ->

1081 map (\(n, ns) ->

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

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

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

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

1078 calls

1084 calls

1079

1085

1080−process h fn (CallsWho n) =

1086+process fn (CallsWho n) =

1081 do calls <- callsWho n

1087 do calls <- callsWho n

1082 ist <- getIState

1088 ist <- getIState

1083− ihRenderResult h . vsep $

1089+ iRenderResult . vsep $

1084 map (\(n, ns) ->

1090 map (\(n, ns) ->

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

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

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

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

1087 calls

1093 calls

1088-- IdrisDoc

1094-- IdrisDoc

1089−process h fn (MakeDoc s) =

1095+process fn (MakeDoc s) =

1090 do istate <- getIState

1096 do istate <- getIState

1091 let names = words s

1097 let names = words s

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

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

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

1143 [] -> return ()

1149 [] -> return ()

1144

1150

1145

1151

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

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

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

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

1148 = idrisCatch

1154 = idrisCatch

1149 (do ist <- getIState

1155 (do ist <- getIState

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

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

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

1196 (\e -> do i <- getIState

1202 (\e -> do i <- getIState

1197 case e of

1203 case e of

1198 At f e' -> do setErrSpan f

1204 At f e' -> do setErrSpan f

1199− ihWarn stdout f $ pprintErr i e'

1205+ iWarn f $ pprintErr i e'

1200 ProgramLineComment -> return () -- fail elsewhere

1206 ProgramLineComment -> return () -- fail elsewhere

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

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

1202− ihWarn stdout emptyFC $ pprintErr i e)

1208+ iWarn emptyFC $ pprintErr i e)

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

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

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

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

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

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

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

1216 then Just l

1222 then Just l

1217 else Nothing

1223 else Nothing

1218 _ -> Nothing

1224 _ -> Nothing

1219− loadFromIFile h f maxline

1225+ loadFromIFile f maxline

1220 inew <- getIState

1226 inew <- getIState

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

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

1222 -- preserve it all from source inputs

1228 -- preserve it all from source inputs

@@ -1326,9 +1332,9 @@ idrisMain opts =

1326 addPkgDir "base"

1332 addPkgDir "base"

1327 mapM_ addPkgDir pkgdirs

1333 mapM_ addPkgDir pkgdirs

1328 elabPrims

1334 elabPrims

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

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

1330 return ()

1336 return ()

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

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

1332 return ()

1338 return ()

1333

1339

1334 when (runrepl && not idesl) initScript

1340 when (runrepl && not idesl) initScript

@@ -1344,14 +1350,14 @@ idrisMain opts =

1344 iputStrLn banner

1350 iputStrLn banner

1345

1351

1346 orig <- getIState

1352 orig <- getIState

1347− loadInputs stdout inputs Nothing

1353+ loadInputs inputs Nothing

1348

1354

1349 runIO $ hSetBuffering stdout LineBuffering

1355 runIO $ hSetBuffering stdout LineBuffering

1350

1356

1351 ok <- noErrors

1357 ok <- noErrors

1352 when ok $ case output of

1358 when ok $ case output of

1353 [] -> return ()

1359 [] -> return ()

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

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

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

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

1356

1362

1357 case immediate of

1363 case immediate of

@@ -1362,7 +1368,7 @@ idrisMain opts =

1362 case parseExpr ist str of

1368 case parseExpr ist str of

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

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

1364 runIO $ exitWith (ExitFailure 1)

1370 runIO $ exitWith (ExitFailure 1)

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

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

1366 exprs

1372 exprs

1367 runIO $ exitWith ExitSuccess

1373 runIO $ exitWith ExitSuccess

1368

1374

@@ -1447,7 +1453,7 @@ initScript = do script <- getInitScript

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

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

1448 Success Proofs -> proofs i

1454 Success Proofs -> proofs i

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

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

1450− Success cmd -> process stdout [] cmd

1456+ Success cmd -> process [] cmd

1451

1457

1452getFile :: Opt -> Maybe String

1458getFile :: Opt -> Maybe String

1453getFile (Filename str) = Just str

1459getFile (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 h -> 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