add a shrink function that can be used to not print all of the output

diff --git a/Main.hs b/Main.hs
index d448264d7de560dc0881b101bdbd7a634ee43b0a..166802b51eb94a42305acd3068f775ddd432d712 100644 (file)
--- a/Main.hs
+++ b/Main.hs
@@ -82,6 +82,9 @@ main = do
     (_,_,errs) -> putStrLn $ "Input error: " ++ concat errs ++ "\n" ++
                              usageInfo usage options
 
+shrink :: String -> String
+shrink s = s -- if length s > 1000 then take 1000 s ++ "..." else s
+
 -- Initialize the main loop
 initLoop :: [Flag] -> FilePath -> History -> IO ()
 initLoop flags f hist = do
@@ -94,9 +97,10 @@ initLoop flags f hist = do
       putStrLn $ "Resolver failed: " ++ err
       runInputT (settings []) (putHistory hist >> loop flags f [] TC.verboseEnv)
     Right (adefs,names) -> do
-      (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs
+      (merr,tenv) <- 
+        TC.runDeclss TC.verboseEnv (takeWhile (\x -> fst (head x) /= "stop") adefs)
       case merr of
-        Just err -> putStrLn $ "Type checking failed: " ++ err
+        Just err -> putStrLn $ "Type checking failed: " ++ shrink err
         Nothing  -> putStrLn "File loaded."
       -- Compute names for auto completion
       runInputT (settings [n | (n,_) <- names]) (putHistory hist >> loop flags f names tenv)
@@ -137,7 +141,7 @@ loop flags f names tenv = do
                 let e = mod $ E.eval (TC.env tenv) body
 
                 -- Let's not crash if the evaluation raises an error:
-                liftIO $ catch (putStrLn (msg ++ show e))
+                liftIO $ catch (putStrLn (msg ++ shrink (show e)))
                                (\e -> putStrLn ("Exception: " ++
                                                 show (e :: SomeException)))
                 stop <- liftIO getCurrentTime

diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt
index 52b504e5ae830af5305106a59ce5fd358a73ac4a..d514a2c7267c64ce73d3a5b61c077679a04f00cd 100644 (file)
--- a/examples/shortsetquot.ctt
+++ b/examples/shortsetquot.ctt
@@ -194,9 +194,6 @@ ntrue' : setquot bool R.1 = (\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(
 
 
 
-
-
-
 -- This is not true:
 -- test' : Id (P' true').1 (K' true')
 --           (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) =