ab32c46 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

ab32c46Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+76−81

compare with master

unifiedsplit

@@ -1276,8 +1276,10 @@ pprintPTerm :: PPOption -- ^^ pretty printing options

1276 -> [FixDecl] -- ^^ Fixity declarations

1277 -> PTerm -- ^^ the term to pretty-print

1278 -> Doc OutputAnnotation

1279−pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1279+pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1280 where

1281+ startPrec = 0

1282+ funcAppPrec = 10

1281 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1283 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1282 prettySe p bnd (PQuote r) =

1284 prettySe p bnd (PQuote r) =

1283 text "![" <> pretty r <> text "]"

1285 text "![" <> pretty r <> text "]"

@@ -1287,21 +1289,21 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1287 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1289 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1288 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1290 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1289 prettySe p bnd (PLam fc n ty sc) =

1291 prettySe p bnd (PLam fc n ty sc) =

1290− bracket p 2 . group . align . hang 2 $

1292+ bracket p startPrec . group . align . hang 2 $

1291 text "\\" <> bindingOf n False <+> text "=>" <$>

1293 text "\\" <> bindingOf n False <+> text "=>" <$>

1292− prettySe 10 ((n, False):bnd) sc

1294+ prettySe startPrec ((n, False):bnd) sc

1293 prettySe p bnd (PLet fc n ty v sc) =

1295 prettySe p bnd (PLet fc n ty v sc) =

1294− bracket p 2 . group . align $

1296+ bracket p startPrec . group . align $

1295− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>

1297+ kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

1296− kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)

1298+ kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

1297 prettySe p bnd (PPi (Exp l s _) n ty sc)

1299 prettySe p bnd (PPi (Exp l s _) n ty sc)

1298 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1300 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1299− bracket p 2 . group $

1301+ bracket p startPrec . group $

1300− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1302+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

1301− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1303+ st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc

1302 | otherwise =

1304 | otherwise =

1303− bracket p 2 . group $

1305+ bracket p startPrec . group $

1304− group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1306+ group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)

1305 where

1307 where

1306 st =

1308 st =

1307 case s of

1309 case s of

@@ -1309,22 +1311,22 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1309 _ -> empty

1311 _ -> empty

1310 prettySe p bnd (PPi (Imp l s _) n ty sc)

1312 prettySe p bnd (PPi (Imp l s _) n ty sc)

1311 | ppopt_impl ppo =

1313 | ppopt_impl ppo =

1312− bracket p 2 $

1314+ bracket p startPrec $

1313− lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1315+ lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1314− st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1316+ st <> text "->" </> prettySe startPrec ((n, True):bnd) sc

1315− | otherwise = prettySe 10 ((n, True):bnd) sc

1317+ | otherwise = prettySe startPrec ((n, True):bnd) sc

1316 where

1318 where

1317 st =

1319 st =

1318 case s of

1320 case s of

1319 Static -> text "[static]" <> space

1321 Static -> text "[static]" <> space

1320 _ -> empty

1322 _ -> empty

1321 prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1323 prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1322− bracket p 2 $

1324+ bracket p startPrec $

1323− prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1325+ prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc

1324 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1326 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1325− bracket p 2 $

1327+ bracket p startPrec $

1326− lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1328+ lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>

1327− rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1329+ rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc

1328 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1330 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1329 | UN nm <- basename f

1331 | UN nm <- basename f

1330 , not (ppopt_impl ppo) && null (getShowArgs args) =

1332 , not (ppopt_impl ppo) && null (getShowArgs args) =

@@ -1337,50 +1339,48 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1337 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1339 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1338 case getShowArgs args of

1340 case getShowArgs args of

1339 [] -> opName True

1341 [] -> opName True

1340− [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))

1342+ [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1341− [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1343+ [l,r] -> let precedence = maybe (startPrec - 1) prec f

1342 in bracket p precedence $ inFix (getTm l) (getTm r)

1344 in bracket p precedence $ inFix (getTm l) (getTm r)

1343 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1345 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1344− bracket p 1 $

1346+ bracket p funcAppPrec $

1345 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1347 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1346 align (group (vsep (map (prettyArgS bnd) rest)))

1348 align (group (vsep (map (prettyArgS bnd) rest)))

1347 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

1349 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

1348 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1350 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1349 f = getFixity (opStr op)

1351 f = getFixity (opStr op)

1350− left l = case f of

1352+ left = case f of

1351− Nothing -> prettySe (-1) bnd l

1353+ Nothing -> funcAppPrec + 1

1352− Just (Infixl p') -> prettySe p' bnd l

1354+ Just (Infixl p') -> p'

1353− Just f' -> prettySe (prec f'-1) bnd l

1355+ Just f' -> prec f' + 1

1354− right r = case f of

1356+ right = case f of

1355− Nothing -> prettySe (-1) bnd r

1357+ Nothing -> funcAppPrec + 1

1356− Just (Infixr p') -> prettySe p' bnd r

1358+ Just (Infixr p') -> p'

1357− Just f' -> prettySe (prec f'-1) bnd r

1359+ Just f' -> prec f' + 1

1358 inFix l r = align . group $

1360 inFix l r = align . group $

1359− (left l <+> opName False) <$> group (right r)

1361+ (prettySe left bnd l <+> opName False) <$>

1362+ group (prettySe right bnd r)

1360 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1363 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1361 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1364 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1362 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1365 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1363− char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1366+ char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))

1364 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1367 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1365 let args = getShowArgs as

1368 let args = getShowArgs as

1366− fp = prettySe 1 bnd f

1369+ fp = prettySe (startPrec + 1) bnd f

1370+ shownArgs = if ppopt_impl ppo then as else args

1367 in

1371 in

1368− bracket p 1 . group $

1372+ bracket p funcAppPrec . group $

1369− if ppopt_impl ppo

1370− then if null as

1373+ if null shownArgs

1371− then fp

1374+ then fp

1372− else fp <+> align (vsep (map (prettyArgS bnd) as))

1375+ else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))

1373− else if null args

1374− then fp

1375− else fp <+> align (vsep (map (prettyArgS bnd) args))

1376 prettySe p bnd (PCase _ scr cases) =

1377− align $ kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <$>

1377+ align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1378 indent 2 (vsep (map ppcase cases))

1379 where

1380+ ppcase (l, r) = let prettyCase = prettySe startPrec

1381+ ([(n, False) | n <- vars l] ++ bnd)

1380− ppcase (l, r) = nest nestingSize $

1382+ in nest nestingSize $

1381− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) l <+>

1383+ prettyCase l <+> text "=>" <+> prettyCase r

1382− text "=>" <+>

1383− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) r

1384 -- Warning: this is a bit of a hack. At this stage, we don't have the

1385 -- global context, so we can't determine which names are constructors,

1386 -- which are types, and which are pattern variables on the LHS of the

@@ -1395,7 +1395,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1395 noNS (NS _ _) = False

1396 noNS _ = True

1397

1398− prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1398+ prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1399 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1400 prettySe p bnd (PResolveTC _) = text "resolvetc"

1401 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

@@ -1403,7 +1403,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1403 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1404 prettySe p bnd (PEq _ lt rt l r)

1405 | ppopt_impl ppo =

1406− bracket p 1 $

1406+ bracket p eqPrec $

1407 enclose lparen rparen eq <+>

1408 align (group (vsep (map (prettyArgS bnd)

1409 [PImp 0 False [] (sUN "A") lt,

@@ -1411,47 +1411,42 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1411 PExp 0 [] (sUN "x") l,

1412 PExp 0 [] (sUN "y") r])))

1413 | otherwise =

1414− bracket p 2 . align . group $

1414+ bracket p eqPrec . align . group $

1415− prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1415+ prettyTerm l <+> eq <$> group (prettyTerm r)

1416 where eq = annName eqTy (text "=")

1417+ eqPrec = startPrec

1418+ prettyTerm = prettySe (eqPrec + 1) bnd

1417 prettySe p bnd (PRewrite _ l r _) =

1419 prettySe p bnd (PRewrite _ l r _) =

1418− bracket p 2 $

1420+ bracket p startPrec $

1419− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1421+ text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r

1420 prettySe p bnd (PTyped l r) =

1422 prettySe p bnd (PTyped l r) =

1421− lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1423+ lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen

1422 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser

1424 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser

1423 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .

1425 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .

1424 align . group . vsep . punctuate (ann comma) $

1426 align . group . vsep . punctuate (ann comma) $

1425− map (prettySe 10 bnd) elts

1427+ map (prettySe startPrec bnd) elts

1426 where ann = case pun of

1428 where ann = case pun of

1427 TypeOrTerm -> id

1429 TypeOrTerm -> id

1428 IsType -> annName pairTy

1430 IsType -> annName pairTy

1429 IsTerm -> annName pairCon

1431 IsTerm -> annName pairCon

1430− prettySe p bnd (PDPair _ TypeOrTerm l t r) =

1432+ prettySe p bnd (PDPair _ pun l t r) =

1431− lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1433+ annotated lparen <>

1432− prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1434+ left <+>

1433− annName sigmaTy lparen <>

1435+ annotated (text "**") <+>

1436+ prettySe startPrec (addBinding bnd) r <>

1437+ annotated rparen

1438+ where annotated = case pun of

1439+ IsType -> annName sigmaTy

1440+ IsTerm -> annName existsCon

1441+ TypeOrTerm -> id

1442+ (left, addBinding) = case (l, pun) of

1434− bindingOf n False <+>

1443+ (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))

1435− annName sigmaTy (text "**") <+>

1436− prettySe 10 ((n, False):bnd) r <>

1437− annName sigmaTy rparen

1438− prettySe p bnd (PDPair _ IsType l t r) =

1439− annName sigmaTy lparen <>

1440− prettySe 10 bnd l <+>

1441− annName sigmaTy (text "**") <+>

1442− prettySe 10 bnd r <>

1444+ _ -> (prettySe startPrec bnd l, id )

1443− annName sigmaTy rparen

1444− prettySe p bnd (PDPair _ IsTerm l t r) =

1445− annName existsCon lparen <>

1446− prettySe 10 bnd l <+>

1447− annName existsCon (text "**") <+>

1448− prettySe 10 bnd r <>

1449− annName existsCon rparen

1450 prettySe p bnd (PAlternative a as) =

1445 prettySe p bnd (PAlternative a as) =

1451 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1446 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1452 where

1447 where

1453 prettyAs =

1448 prettyAs =

1454− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

1449+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1455 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1450 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1456 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1451 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1457 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1452 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

@@ -1479,10 +1474,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1479 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1474 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1480 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1475 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1481

1476

1482− prettyArgSe bnd arg = prettySe 0 bnd arg

1477+ prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg

1483− prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1478+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace

1484− prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1479+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace

1485− prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1480+ prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace

1486

1481

1487 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1482 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1488 annName n = annotate (AnnName n Nothing Nothing Nothing)

1483 annName n = annotate (AnnName n Nothing Nothing Nothing)

@@ -1539,7 +1534,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1539 snat _ _ = Nothing

1534 snat _ _ = Nothing

1540

1535

1541 bracket outer inner doc

1536 bracket outer inner doc

1542− | inner > outer = lparen <> doc <> rparen

1537+ | outer > inner = lparen <> doc <> rparen

1543 | otherwise = doc

1538 | otherwise = doc

1544

1539

1545 kwd = annotate AnnKeyword . text

1540 kwd = annotate AnnKeyword . text

src/Idris/REPL.hs+14−13

@@ -309,8 +309,8 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

309 clearErr

310 putIState (orig { idris_options = idris_options i,

311 idris_outputmode = (IdeSlave id h) })

312− loadInputs [filename] toline

312+ mods <- loadInputs [filename] toline

313− isetPrompt (mkPrompt [filename])

313+ isetPrompt (mkPrompt mods)

314 -- Report either success or failure

315 i <- getIState

316 case (errSpan i) of

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

321 (idris_parsedSpan i)

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

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

324− ideslave h orig [filename]

324+ ideslave h orig mods

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

326 case splitName name of

327 Left err -> iPrintError err

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

622 }

623 clearErr

624 mods <- loadInputs inputs Nothing

625− return (Just inputs)

625+ return (Just mods)

626 Success (Right (Load f toline)) ->

627 do putIState orig { idris_options = idris_options i

628 , idris_colourTheme = idris_colourTheme i

629 }

630 clearErr

631 mod <- loadInputs [f] toline

632− return (Just [f])

632+ return (Just mod)

633 Success (Right (ModImport f)) ->

634 do clearErr

635 fmod <- loadModule f

@@ -1334,7 +1334,7 @@ idris opts = do res <- runExceptT $ execStateT totalMain idrisInit

1334 [] -> return ()

1335

1336

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

1337+loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

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

1339 = idrisCatch

1340 (do ist <- getIState

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

1363 when (not (all ibc ifiles) || loadCode) $

1364 tryLoad False (filter (not . ibc) ifiles)

1365 -- return the files that need rechecking

1366− return ifiles)

1366+ return (input, ifiles))

1367 ninputs

1368 inew <- getIState

1369 let tidata = idris_tyinfodata inew

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

1372 case errSpan inew of

1373 Nothing ->

1374 do putIState (ist { idris_tyinfodata = tidata })

1375− ibcfiles <- mapM findNewIBC (nub (concat ifiles))

1375+ ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

1376 tryLoad True (mapMaybe id ibcfiles)

1377 _ -> return ()

1378 ist <- getIState

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

1383 [] -> performUsageAnalysis -- interactive

1384 _ -> return [] -- batch, will be checked by the compiler

1385

1386− return ())

1386+ return (map fst ifiles))

1387 (\e -> do i <- getIState

1388 case e of

1389 At f e' -> do setErrSpan f

@@ -1392,7 +1392,8 @@ loadInputs inputs toline -- furthest line to read in input source files

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

1393 -- Issue #1576 on the issue tracker.

1394 -- https://github.com/idris-lang/Idris-dev/issues/1576

1395− iWarn emptyFC $ pprintErr i e)

1395+ iWarn emptyFC $ pprintErr i e

1396+ return [])

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

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

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

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

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

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

@@ -1538,7 +1539,7 @@ idrisMain opts =

1538 iputStrLn banner

1539 iputStrLn banner

1539

1540

1540 orig <- getIState

1541 orig <- getIState

1541− when (not idesl) $ loadInputs inputs Nothing

1542+ mods <- if idesl then return [] else loadInputs inputs Nothing

1542

1543

1543 runIO $ hSetBuffering stdout LineBuffering

1544 runIO $ hSetBuffering stdout LineBuffering

1544

1545

@@ -1580,8 +1581,8 @@ idrisMain opts =

1580

1581

1581 when (runrepl && not idesl) $ do

1582 when (runrepl && not idesl) $ do

1582-- clearOrigPats

1583-- clearOrigPats

1583− startServer port orig inputs

1584+ startServer port orig mods

1584− runInputT (replSettings (Just historyFile)) $ repl orig inputs

1585+ runInputT (replSettings (Just historyFile)) $ repl orig mods

1585 let idesock = IdeslaveSocket `elem` opts

1586 let idesock = IdeslaveSocket `elem` opts

1586 when (idesl) $ ideslaveStart idesock orig inputs

1587 when (idesl) $ ideslaveStart idesock orig inputs

1587 ok <- noErrors

1588 ok <- noErrors