X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=2f36fc647a065479bf6c553f6a4cfbdf1dcd557c;hb=18ad62cacbbb08decd4332b0bab449e640114fd7;hp=4735fdd4a8e0d5533ddca47778b3ced323ff0295;hpb=c4afa186c53998a10eab85d3fcc113b07bccfdf9;p=helm.git

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 4735fdd4a..2f36fc647 100644
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -27,10 +27,12 @@ open Printf
 
 open MatitaTypes
 
+type callback = string -> command_outcome
+
 (* let default_prompt = "# " *)
 let default_prompt = ""
 let default_phrase_sep = "."
-let default_callback = fun (phrase: string) -> true
+let default_callback = fun (phrase: string) -> (true, true)
 let bullet = "∙"
 
 let message_props = [ `STYLE `ITALIC ]
@@ -146,12 +148,8 @@ class console
 
     method private invoke_callback phrase =
       history#add phrase;
-      if _callback phrase then begin
-        self#hide ();
-        self#clear ()
-      end
-        (* else callback encountered troubles, don't hide console which
-        probably contains error message *)
+      let (success, hide) = _callback phrase in
+      if hide then self#hide ()
 
     method clear () =
       let buf = self#buffer in
@@ -216,33 +214,28 @@ class console
     method private next_phrase =
       try self#set_phrase history#next with History_failure -> ()
 
-    method wrap_exn (f: unit -> unit) =
-      try
-        f ();
-        true
-      with
-      | StatefulProofEngine.Tactic_failure exn ->
-          self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn));
-          false
-      | CicTextualParser2.Parse_error (floc, msg) ->
-          let buf = self#buffer in
-          let (x, y) = CicAst.loc_of_floc floc in
-          let red = buf#create_tag [`FOREGROUND "red"] in
-          let (start_error_pos, end_error_pos) =
-            buf#end_iter#backward_chars (String.length last_phrase - x),
-            buf#end_iter#backward_chars (String.length last_phrase - y)
-          in
-          if x - y = 0 then (* no region to highlight, let's add an hint about
-                            where the error occured *)
-            buf#insert ~iter:end_error_pos ~tags:[red] bullet
-          else  (* highlight the region where the error occured *)
-            buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos;
-          self#echo_error (sprintf "at character %d-%d: %s" x y msg);
-          false
-      | exn ->
-          self#echo_error (sprintf "Uncaught exception: %s"
-            (Printexc.to_string exn));
-          false
+    method wrap_exn: 'a. (unit -> 'a) -> 'a option =
+      fun f ->
+        try
+          Some (f ())
+        with exn ->
+          (match exn with (* highlight parse errors in user input *)
+          | CicTextualParser2.Parse_error (floc, msg) ->
+              let buf = self#buffer in
+              let (x, y) = CicAst.loc_of_floc floc in
+              let red = buf#create_tag [`FOREGROUND "red"] in
+              let (start_error_pos, end_error_pos) =
+                buf#end_iter#backward_chars (String.length last_phrase - x),
+                buf#end_iter#backward_chars (String.length last_phrase - y)
+              in
+              if x - y = 0 then (* no region to highlight, let's add an hint
+                                about where the error occured *)
+                buf#insert ~iter:end_error_pos ~tags:[red] bullet
+              else  (* highlight the region where the error occured *)
+                buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos;
+          | _ -> ());
+          self#echo_error (explain exn);
+          None
 
   end