snapshot

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 3a4295f4ac99f94f8d75eca3ff94953f22d8b4ba..5933f6227124a6f3709d3c90e5d7b0e551747c1e 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -219,6 +219,7 @@ class proofState
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
+  ~(dbd: Mysql.dbd)
   ()
 =
   let disambiguate ast =
@@ -251,6 +252,7 @@ class proofState
     | TacticAst.Replace (what, with_what) ->
         Tactics.replace ~what:(disambiguate what)
           ~with_what:(disambiguate with_what)
+    | TacticAst.Auto -> Tactics.auto_new ~dbd
   (*
     (* TODO Zack a lot more of tactics to be implemented here ... *)
     | TacticAst.Change of 'term * 'term * 'ident option
@@ -318,23 +320,14 @@ class interpreter
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
+  ~(dbd: Mysql.dbd)
   ()
 =
   let commandState =
     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
+  let proofState =
+    new proofState ~disambiguator ~proof_handler ~console ~dbd ()
   in
   object (self)
     val mutable state = commandState
@@ -348,11 +341,18 @@ class interpreter
       | Some `Proof -> state <- proofState
       | None -> ()
 
-    method evalPhrase ?(transparent = false) s =
-      wrap_exn transparent (fun () -> self#updateState (state#evalPhrase s))
-
-    method evalAst ?(transparent = false) s =
-      wrap_exn transparent (fun () -> self#updateState (state#evalAst s))
-
+    method evalPhrase s =
+      let success =
+        console#wrap_exn (fun () -> self#updateState (state#evalPhrase s))
+      in
+      if success then console#clear ();
+      success
+
+    method evalAst ast =
+      let success =
+        console#wrap_exn (fun () -> self#updateState (state#evalAst ast))
+      in
+      if success then console#clear ();
+      success
   end