@@ -308,8 +308,8 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =
309 putIState (orig { idris_options = idris_options i,
309 putIState (orig { idris_options = idris_options i,
310 idris_outputmode = (IdeSlave id h) })
310 idris_outputmode = (IdeSlave id h) })
311− loadInputs [filename] toline
311+ mods <- loadInputs [filename] toline
312− isetPrompt (mkPrompt [filename])
312+ isetPrompt (mkPrompt mods)
313 -- Report either success or failure
313 -- Report either success or failure
314 i <- getIState
314 i <- getIState
315 case (errSpan i) of
315 case (errSpan i) of
@@ -320,7 +320,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =
320 (idris_parsedSpan i)
320 (idris_parsedSpan i)
321 in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
321 in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id
322 Just x -> iPrintError $ "didn't load " ++ filename
322 Just x -> iPrintError $ "didn't load " ++ filename
323− ideslave h orig [filename]
323+ ideslave h orig mods
324runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =
324runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =
325 case splitName name of
325 case splitName name of
326 Left err -> iPrintError err
326 Left err -> iPrintError err
@@ -621,14 +621,14 @@ processInput cmd orig inputs
623 mods <- loadInputs inputs Nothing
623 mods <- loadInputs inputs Nothing
624− return (Just inputs)
624+ return (Just mods)
625 Success (Right (Load f toline)) ->
625 Success (Right (Load f toline)) ->
626 do putIState orig { idris_options = idris_options i
626 do putIState orig { idris_options = idris_options i
627 , idris_colourTheme = idris_colourTheme i
627 , idris_colourTheme = idris_colourTheme i
630 mod <- loadInputs [f] toline
630 mod <- loadInputs [f] toline
631− return (Just [f])
631+ return (Just mod)
632 Success (Right (ModImport f)) ->
632 Success (Right (ModImport f)) ->
633 do clearErr
633 do clearErr
634 fmod <- loadModule f
634 fmod <- loadModule f
@@ -1328,7 +1328,7 @@ idris opts = do res <- runExceptT $ execStateT totalMain idrisInit
1328 [] -> return ()
1328 [] -> return ()
1331−loadInputs :: [FilePath] -> Maybe Int -> Idris ()
1331+loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
1332loadInputs inputs toline -- furthest line to read in input source files
1332loadInputs inputs toline -- furthest line to read in input source files
1333 = idrisCatch
1333 = idrisCatch
1334 (do ist <- getIState
1334 (do ist <- getIState
@@ -1357,7 +1357,7 @@ loadInputs inputs toline -- furthest line to read in input source files
1357 when (not (all ibc ifiles) || loadCode) $
1357 when (not (all ibc ifiles) || loadCode) $
1358 tryLoad False (filter (not . ibc) ifiles)
1358 tryLoad False (filter (not . ibc) ifiles)
1359 -- return the files that need rechecking
1359 -- return the files that need rechecking
1360− return ifiles)
1360+ return (input, ifiles))
1362 inew <- getIState
1362 inew <- getIState
1363 let tidata = idris_tyinfodata inew
1363 let tidata = idris_tyinfodata inew
@@ -1366,7 +1366,7 @@ loadInputs inputs toline -- furthest line to read in input source files
1366 case errSpan inew of
1366 case errSpan inew of
1367 Nothing ->
1367 Nothing ->
1368 do putIState (ist { idris_tyinfodata = tidata })
1368 do putIState (ist { idris_tyinfodata = tidata })
1369− ibcfiles <- mapM findNewIBC (nub (concat ifiles))
1369+ ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))
1370 tryLoad True (mapMaybe id ibcfiles)
1370 tryLoad True (mapMaybe id ibcfiles)
1371 _ -> return ()
1371 _ -> return ()
1372 ist <- getIState
1372 ist <- getIState
@@ -1377,7 +1377,7 @@ loadInputs inputs toline -- furthest line to read in input source files
1377 [] -> performUsageAnalysis -- interactive
1377 [] -> performUsageAnalysis -- interactive
1378 _ -> return [] -- batch, will be checked by the compiler
1378 _ -> return [] -- batch, will be checked by the compiler
1380− return ())
1380+ return (map fst ifiles))
1381 (\e -> do i <- getIState
1381 (\e -> do i <- getIState
1382 case e of
1382 case e of
1383 At f e' -> do setErrSpan f
1383 At f e' -> do setErrSpan f
@@ -1386,7 +1386,8 @@ loadInputs inputs toline -- furthest line to read in input source files
1386 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1386 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1387 -- Issue #1576 on the issue tracker.
1387 -- Issue #1576 on the issue tracker.
1388 -- https://github.com/idris-lang/Idris-dev/issues/1576
1388 -- https://github.com/idris-lang/Idris-dev/issues/1576
1389− iWarn emptyFC $ pprintErr i e)
1389+ iWarn emptyFC $ pprintErr i e
1390 where -- load all files, stop if any fail
1391 where -- load all files, stop if any fail
1391 tryLoad :: Bool -> [IFileType] -> Idris ()
1392 tryLoad :: Bool -> [IFileType] -> Idris ()
1392 tryLoad keepstate [] = warnTotality >> return ()
1393 tryLoad keepstate [] = warnTotality >> return ()
@@ -1532,7 +1533,7 @@ idrisMain opts =
1532 iputStrLn banner
1533 iputStrLn banner
1534 orig <- getIState
1535 orig <- getIState
1535− when (not idesl) $ loadInputs inputs Nothing
1536+ mods <- if idesl then return [] else loadInputs inputs Nothing
1537 runIO $ hSetBuffering stdout LineBuffering
1538 runIO $ hSetBuffering stdout LineBuffering
@@ -1570,8 +1571,8 @@ idrisMain opts =
1571 when (runrepl && not idesl) $ do
1572 when (runrepl && not idesl) $ do
1572-- clearOrigPats
1573-- clearOrigPats
1573− startServer port orig inputs
1574+ startServer port orig mods
1574− runInputT (replSettings (Just historyFile)) $ repl orig inputs
1575+ runInputT (replSettings (Just historyFile)) $ repl orig mods
1575 let idesock = IdeslaveSocket `elem` opts
1576 let idesock = IdeslaveSocket `elem` opts
1576 when (idesl) $ ideslaveStart idesock orig inputs
1577 when (idesl) $ ideslaveStart idesock orig inputs
1577 ok <- noErrors
1578 ok <- noErrors