2e02cf6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Logging options

commit2e02cf6748aa005948331710fd89cebc9c6172bd authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 15 Nov 2011, 10:46 (15 years ago) parent74183cb

3 files changed+10−9

compare with master

unifiedsplit

samples/interp.idr+1−2 src/Idris/Parser.hs+8−6 src/Idris/REPL.hs+1−1

samples/interp.idr+1−2

@@ -27,7 +27,6 @@ using (G : Vect Ty n) {

2727 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

2828 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

2929

30−

3130 interp : Env G -> [static] Expr G t -> interpTy t;

3231 interp env (Var i) = envLookup i env;

3332 interp env (Val x) = x;

@@ -40,7 +39,7 @@ using (G : Vect Ty n) {

4039

4140 eId : Expr G (TyFun TyInt TyInt);

4241 eId = Lam (Var fO);

43−

42+

4443 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

4544 eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

4645

src/Idris/Parser.hs+8−6

@@ -675,12 +675,14 @@ pWhereblock n syn

675675 return (concat ds, map (\x -> (x, decoration syn x)) dns)

676676

677677pDirective :: IParser [PDecl]

678−pDirective = do lchar '%'; reserved "lib"; lib <- strlit;

679− return [PDirective (addLib lib)]

680− <|> do lchar '%'; reserved "link"; obj <- strlit;

681− return [PDirective (do datadir <- lift $ getDataDir

682− o <- lift $ findInPath [".", datadir] obj

683− addObjectFile o)]

678+pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

679+ return [PDirective (addLib lib)])

680+ <|> try (do lchar '%'; reserved "link"; obj <- strlit;

681+ return [PDirective (do datadir <- lift $ getDataDir

682+ o <- lift $ findInPath [".", datadir] obj

683+ addObjectFile o)])

684+ <|> do lchar '%'; reserved "logging"; i <- natural;

685+ return [PDirective (setLogLevel (fromInteger i))]

684686

685687pTactic :: SyntaxInfo -> IParser PTactic

686688pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

src/Idris/REPL.hs+1−1

@@ -52,7 +52,7 @@ processInput cmd orig inputs

5252 case parseCmd i cmd of

5353 Left err -> do lift $ print err

5454 return (Just inputs)

55− Right Reload -> do put orig

55+ Right Reload -> do put (orig { idris_options = idris_options i })

5656 clearErr

5757 mods <- mapM loadModule inputs

5858 return (Just inputs)