snapshot:

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 35ec6119d2bf4d781fcf0c7c6e386da915e5dd6a..3a4295f4ac99f94f8d75eca3ff94953f22d8b4ba 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -113,18 +113,12 @@ class virtual interpreterState =
     method virtual evalTactical:
       (CicAst.term, string) TacticAst.tactical -> state_tag
 
-(*
-    method undo ?(steps = 1) () =
-      for i = 1 to steps do
-        match List.hd !history with
-        | `Qed 
-        FINQUI
-*)
-
     method evalPhrase s =
       debug_print (sprintf "evaluating '%s'" s);
       self#evalTactical (self#parsePhrase s)
 
+    method evalAst ast = self#evalTactical ast
+
     method endOffset =
       match !loc with
       | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum
@@ -330,6 +324,18 @@ class interpreter
     new commandState ~disambiguator ~proof_handler ~console ()
   in
   let proofState = new proofState ~disambiguator ~proof_handler ~console () in
+  let wrap_exn transparent f =
+    try
+      f ();
+      true
+    with exn ->
+      if transparent then
+        raise exn
+      else
+        console#echo_error (sprintf "Uncaught exception: %s"
+          (Printexc.to_string exn));
+      false
+  in
   object (self)
     val mutable state = commandState
 
@@ -343,14 +349,10 @@ class interpreter
       | None -> ()
 
     method evalPhrase ?(transparent = false) s =
-      try
-        self#updateState (state#evalPhrase s)
-      with exn ->
-        if transparent then
-          raise exn
-        else
-          console#echo_error (sprintf "Uncaught exception: %s"
-            (Printexc.to_string exn))
+      wrap_exn transparent (fun () -> self#updateState (state#evalPhrase s))
+
+    method evalAst ?(transparent = false) s =
+      wrap_exn transparent (fun () -> self#updateState (state#evalAst s))
 
   end