on master help sign in
Prevent REPL from compiling to source file
commit52f8587151103fd854c3b65b7a519afc795fe837 authorSebastian de Bellefon <arnaudpourseb@gmail.com> dateThu 18 Sep 2014, 04:36 (12 years ago) parentf50a883
1 file changed+8−6
src/Idris/REPL.hs+8−6
src/Idris/REPL.hs+8−6
@@ -1054,12 +1054,14 @@ process fn Execute
10541054 (\e -> getIState >>= iRenderError . flip pprintErr e)
10551055 where fc = fileFC "main"
10561056process fn (Compile codegen f)
1057− = do (m, _) <- elabVal recinfo ERHS
1058− (PApp fc (PRef fc (sUN "run__IO"))
1059− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1060− ir <- compile codegen f m
1061− i <- getIState
1062− runIO $ generate codegen (head (idris_imported i)) ir
1057+ = if map toLower (takeExtension f) `elem` [".idr", ".idc"]
1058+ then runIO $ putStrLn ("Will not compile to " ++ f)
1059+ else do (m, _) <- elabVal recinfo ERHS
1060+ (PApp fc (PRef fc (sUN "run__IO"))
1061+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
1062+ ir <- compile codegen f m
1063+ i <- getIState
1064+ runIO $ generate codegen (head (idris_imported i)) ir
10631065 where fc = fileFC "main"
10641066process fn (LogLvl i) = setLogLevel i
10651067-- Elaborate as if LHS of a pattern (debug command)