]> matita.cs.unibo.it Git - helm.git/commitdiff
A few bug fixes. In particular parsing errors in matitatop when a file is
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jun 2005 14:34:20 +0000 (14:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jun 2005 14:34:20 +0000 (14:34 +0000)
given to process used to result in entering the ocaml mode. Now the user is
left in the matita mode.

helm/matita/matitacLib.ml

index 1baa34910c3a1356d5c08b0b3133a9e28a1e7f30..d57d211e21edde02b8c20beae7c5468f068e9bbb 100644 (file)
@@ -98,6 +98,7 @@ let rec go () =
      else
       let (x, y) = CicAst.loc_of_floc floc in
       MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+      go ()
   | exn -> MatitaLog.error (Printexc.to_string exn); go ()
   
 let main ~mode = 
@@ -153,5 +154,7 @@ let main ~mode =
      let (x, y) = CicAst.loc_of_floc floc in
      MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
      Http_getter.sync_dump_file ();
-     exit 1
-  
+     if mode = `COMPILER then
+       exit 1
+     else
+       go ()