snapshot, notably:

[helm.git] / helm / matita / matitac.ml

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 3f394cdb1108e9dc70158ad99d51c66b714bccc0..87c30cfea08001eca25930502198dcad170e4468 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -78,16 +78,20 @@ let disambiguator =
     ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback
     ()
 let console = new tty_console
-let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof)
-let interpreter =
-  new MatitaInterpreter.interpreter
-    ~disambiguator ~currentProof ~console ~dbd ()
+let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console ()
 
 let run_script fname =
   message (sprintf "execution of %s started:" fname);
   let script =
     let ic = open_in fname in
-    let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in
+    let ast = 
+      try 
+        snd (CicTextualParser2.parse_script (Stream.of_channel ic)) 
+      with
+        exn -> 
+          error (explain exn); 
+          assert false (* should be something like (Unix.exit 1) *)
+    in
     close_in ic;
     ast
   in