602552e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add :loadto command

602552eEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+3−2

compare with master

unifiedsplit

@@ -291,7 +291,7 @@ data Command = Quit

291 | DocStr (Either Name Const)

292 | TotCheck Name

293 | Reload

294− | Load FilePath

294+ | Load FilePath (Maybe Int) -- up to maximum line number

295 | ChangeDirectory FilePath

296 | ModImport String

297 | Edit

@@ -960,6 +960,7 @@ data SyntaxInfo = Syn { using :: [Using],

960 decoration :: Name -> Name,

961 inPattern :: Bool,

962 implicitAllowed :: Bool,

963+ maxline :: Maybe Int,

963 dsl_info :: DSL }

964 dsl_info :: DSL }

964 deriving Show

965 deriving Show

965{-!

966{-!

@@ -967,7 +968,7 @@ deriving instance NFData SyntaxInfo

967deriving instance Binary SyntaxInfo

968deriving instance Binary SyntaxInfo

968!-}

969!-}

969

970

970−defaultSyntax = Syn [] [] [] [] id False False initDSL

971+defaultSyntax = Syn [] [] [] [] id False False Nothing initDSL

971

972

972expandNS :: SyntaxInfo -> Name -> Name

973expandNS :: SyntaxInfo -> Name -> Name

973expandNS syn n@(NS _ _) = n

974expandNS syn n@(NS _ _) = n

src/Idris/DeepSeq.hs+2−2

@@ -321,11 +321,11 @@ instance NFData Using where

321

322

323instance NFData SyntaxInfo where

324− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8)

324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9)

325 = rnf x1 `seq`

326 rnf x2 `seq`

327 rnf x3 `seq`

328− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

328+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

329

330

331

src/Idris/IBC.hs+2−2

@@ -1573,7 +1573,7 @@ instance Binary Using where

1573 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1574

1575instance Binary SyntaxInfo where

1576− put (Syn x1 x2 x3 x4 _ x5 x6 x7)

1576+ put (Syn x1 x2 x3 x4 _ x5 x6 _ x7)

1577 = do put x1

1578 put x2

1579 put x3

@@ -1589,7 +1589,7 @@ instance Binary SyntaxInfo where

1589 x5 <- get

1590 x6 <- get

1591 x7 <- get

1592− return (Syn x1 x2 x3 x4 id x5 x6 x7)

1592+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing x7)

1593

1594instance (Binary t) => Binary (PClause' t) where

1595 put x

src/Idris/Parser.hs+28−18

@@ -128,9 +128,10 @@ import_ = do fc <- getFC

128prog :: SyntaxInfo -> IdrisParser [PDecl]

129prog syn = do whiteSpace

130 decls <- many (decl syn)

131− notOpenBraces

132− eof

133 let c = (concat decls)

131 let c = (concat decls)

132+ case maxline syn of

133+ Nothing -> do notOpenBraces; eof

134+ _ -> return ()

134 return c

135 return c

135

136

136{-| Parses a top-level declaration

137{-| Parses a top-level declaration

@@ -153,8 +154,16 @@ Decl ::=

153@

154@

154-}

155-}

155decl :: SyntaxInfo -> IdrisParser [PDecl]

156decl :: SyntaxInfo -> IdrisParser [PDecl]

156−decl syn = do notEndBlock

157+decl syn = do fc <- getFC

158+ -- if we're after maxline, stop here

159+ let continue = case maxline syn of

160+ Nothing -> True

161+ Just l -> if fst (fc_end fc) > l

162+ then False

163+ else True

164+ if continue then do notEndBlock

157− declBody

165+ declBody

166+ else fail "End of readable input"

158 where declBody :: IdrisParser [PDecl]

167 where declBody :: IdrisParser [PDecl]

159 declBody = declBody'

168 declBody = declBody'

160 <|> using_ syn

169 <|> using_ syn

@@ -1177,21 +1186,21 @@ loadModule' outh f

1177 then iLOG $ "Already read " ++ file

1186 then iLOG $ "Already read " ++ file

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

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

1179 case fp of

1188 case fp of

1180− IDR fn -> loadSource outh False fn

1189+ IDR fn -> loadSource outh False fn Nothing

1181− LIDR fn -> loadSource outh True fn

1190+ LIDR fn -> loadSource outh True fn Nothing

1182 IBC fn src ->

1191 IBC fn src ->

1183 idrisCatch (loadIBC fn)

1192 idrisCatch (loadIBC fn)

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

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

1185 case src of

1194 case src of

1186− IDR sfn -> loadSource outh False sfn

1195+ IDR sfn -> loadSource outh False sfn Nothing

1187− LIDR sfn -> loadSource outh True sfn)

1196+ LIDR sfn -> loadSource outh True sfn Nothing)

1188 let (dir, fh) = splitFileName file

1197 let (dir, fh) = splitFileName file

1189 return (dropExtension fh)

1198 return (dropExtension fh)

1190

1199

1191

1200

1192{- | Load idris code from file -}

1201{- | Load idris code from file -}

1193−loadFromIFile :: Handle -> IFileType -> Idris ()

1202+loadFromIFile :: Handle -> IFileType -> Maybe Int -> Idris ()

1194−loadFromIFile h i@(IBC fn src)

1203+loadFromIFile h i@(IBC fn src) maxline

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

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

1196 idrisCatch (loadIBC fn)

1205 idrisCatch (loadIBC fn)

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

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

@@ -1200,13 +1209,13 @@ loadFromIFile h i@(IBC fn src)

1200 getSrcFile (LIDR fn) = fn

1209 getSrcFile (LIDR fn) = fn

1201 getSrcFile (IBC f src) = getSrcFile src

1210 getSrcFile (IBC f src) = getSrcFile src

1202

1211

1203−loadFromIFile h (IDR fn) = loadSource' h False fn

1212+loadFromIFile h (IDR fn) maxline = loadSource' h False fn maxline

1204−loadFromIFile h (LIDR fn) = loadSource' h True fn

1213+loadFromIFile h (LIDR fn) maxline = loadSource' h True fn maxline

1205

1214

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

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

1207−loadSource' :: Handle -> Bool -> FilePath -> Idris ()

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

1208−loadSource' h lidr r

1217+loadSource' h lidr r maxline

1209− = idrisCatch (loadSource h lidr r)

1218+ = idrisCatch (loadSource h lidr r maxline)

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

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

1211 ist <- getIState

1220 ist <- getIState

1212 case e of

1221 case e of

@@ -1214,8 +1223,8 @@ loadSource' h lidr r

1214 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

1223 _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

1215

1224

1216{- | Load Idris source code-}

1225{- | Load Idris source code-}

1217−loadSource :: Handle -> Bool -> FilePath -> Idris ()

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

1218−loadSource h lidr f

1227+loadSource h lidr f toline

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

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

1220 i <- getIState

1229 i <- getIState

1221 let def_total = default_total i

1230 let def_total = default_total i

@@ -1246,7 +1255,8 @@ loadSource h lidr f

1246 putIState (i { default_access = Hidden, module_aliases = modAliases })

1255 putIState (i { default_access = Hidden, module_aliases = modAliases })

1247 clearIBC -- start a new .ibc file

1256 clearIBC -- start a new .ibc file

1248 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1257 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1249− let syntax = defaultSyntax{ syn_namespace = reverse mname }

1258+ let syntax = defaultSyntax{ syn_namespace = reverse mname,

1259+ maxline = toline }

1250 ds' <- parseProg syntax f file pos

1260 ds' <- parseProg syntax f file pos

1251

1261

1252 -- Parsing done, now process declarations

1262 -- Parsing done, now process declarations

src/Idris/REPL.hs+28−13

@@ -166,8 +166,8 @@ processNetCmd orig i h fn cmd

166 Left err -> do hPutStrLn h (show err)

167 return (i, fn)

168 where

169− processNet fn Reload = processNet fn (Load fn)

169+ processNet fn Reload = processNet fn (Load fn Nothing)

170− processNet fn (Load f) =

170+ processNet fn (Load f toline) =

171 do let ist = orig { idris_options = idris_options i

172 , idris_colourTheme = idris_colourTheme i

173 , idris_colourRepl = False

@@ -177,7 +177,7 @@ processNetCmd orig i h fn cmd

177 setOutH h

178 setQuiet True

179 setVerbose False

180− mods <- loadInputs h [f]

180+ mods <- loadInputs h [f] toline

181 ist <- getIState

182 return (ist, f)

183 processNet fn c = do process h fn c

@@ -258,7 +258,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =

258 clearErr

259 putIState (orig { idris_options = idris_options i,

260 idris_outputmode = (IdeSlave id) })

261− loadInputs stdout [filename]

261+ loadInputs stdout [filename] Nothing

262 isetPrompt (mkPrompt [filename])

263 -- Report either success or failure

264 i <- getIState

@@ -474,14 +474,14 @@ processInput cmd orig inputs

474 , idris_colourTheme = idris_colourTheme i

475 }

476 clearErr

477− mods <- loadInputs stdout inputs

477+ mods <- loadInputs stdout inputs Nothing

478 return (Just inputs)

479− Success (Load f) ->

479+ Success (Load f toline) ->

480 do putIState orig { idris_options = idris_options i

481 , idris_colourTheme = idris_colourTheme i

482 }

483 clearErr

484− mod <- loadInputs stdout [f]

484+ mod <- loadInputs stdout [f] toline

485 return (Just [f])

486 Success (ModImport f) ->

487 do clearErr

@@ -530,7 +530,7 @@ edit f orig

530 putIState $ orig { idris_options = idris_options i

531 , idris_colourTheme = idris_colourTheme i

532 }

533− loadInputs stdout [f]

533+ loadInputs stdout [f] Nothing

534-- clearOrigPats

535 iucheck

536 return ()

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

994 [] -> return ()

995

996

997−loadInputs :: Handle -> [FilePath] -> Idris ()

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

998−loadInputs h inputs

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

999 = idrisCatch

1000 (do ist <- getIState

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

@@ -1056,7 +1056,18 @@ loadInputs h inputs

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

1057 tryLoad keepstate (f : fs)

1058 = do ist <- getIState

1059+ let maxline

1060+ = case toline of

1061+ Nothing -> Nothing

1062+ Just l -> case f of

1063+ IDR fn -> if any (fmatch fn) inputs

1064+ then Just l

1065+ else Nothing

1066+ LIDR fn -> if any (fmatch fn) inputs

1067+ then Just l

1068+ else Nothing

1069+ _ -> Nothing

1059− loadFromIFile h f

1070+ loadFromIFile h f maxline

1060 inew <- getIState

1071 inew <- getIState

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

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

1062 -- preserve it all from source inputs

1073 -- preserve it all from source inputs

@@ -1072,6 +1083,10 @@ loadInputs h inputs

1072 ibc (IBC _ _) = True

1083 ibc (IBC _ _) = True

1073 ibc _ = False

1084 ibc _ = False

1074

1085

1086+ fmatch ('.':'/':xs) ys = fmatch xs ys

1087+ fmatch xs ('.':'/':ys) = fmatch xs ys

1088+ fmatch xs ys = xs == ys

1089+

1075 findNewIBC :: IFileType -> Idris (Maybe IFileType)

1090 findNewIBC :: IFileType -> Idris (Maybe IFileType)

1076 findNewIBC i@(IBC _ _) = return (Just i)

1091 findNewIBC i@(IBC _ _) = return (Just i)

1077 findNewIBC s@(IDR f) = do ist <- get

1092 findNewIBC s@(IDR f) = do ist <- get

@@ -1181,7 +1196,7 @@ idrisMain opts =

1181 iputStrLn banner

1196 iputStrLn banner

1182

1197

1183 orig <- getIState

1198 orig <- getIState

1184− loadInputs stdout inputs

1199+ loadInputs stdout inputs Nothing

1185

1200

1186 runIO $ hSetBuffering stdout LineBuffering

1201 runIO $ hSetBuffering stdout LineBuffering

1187

1202

@@ -1278,7 +1293,7 @@ initScript = do script <- getInitScript

1278 case parseCmd i input cmd of

1293 case parseCmd i input cmd of

1279 Failure err -> runIO $ print (fixColour clr err)

1294 Failure err -> runIO $ print (fixColour clr err)

1280 Success Reload -> iPrintError "Init scripts cannot reload the file"

1295 Success Reload -> iPrintError "Init scripts cannot reload the file"

1281− Success (Load f) -> iPrintError "Init scripts cannot load files"

1296+ Success (Load f _) -> iPrintError "Init scripts cannot load files"

1282 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"

1297 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"

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

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

1284 Success Proofs -> proofs i

1299 Success Proofs -> proofs i

src/Idris/REPLParser.hs+6−1

@@ -48,7 +48,12 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

48 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

49 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

50 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

51+ <|> try (do cmd ["lto", "loadto"];

52+ toline <- P.natural

53+ f <- many anyChar;

54+ return (Load f (Just (fromInteger toline))))

51− <|> try (do cmd ["l", "load"]; f <- many anyChar; return (Load f))

55+ <|> try (do cmd ["l", "load"]; f <- many anyChar;

56+ return (Load f Nothing))

52 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

57 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

53 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

58 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

54 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

59 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))