X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.ml;h=3d40e949ee46ae156abe5e34625c7dbac8346fc2;hb=f38e8fafcf040258b54b4032562753a876a8a94e;hp=889d8e2d80244eb0aa23062347f4875819a6c401;hpb=5ee4e9d9fbff19b7937459c5ad4652542ac1ccb8;p=helm.git

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 889d8e2d8..3d40e949e 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
@@ -172,6 +170,7 @@ class console
       self#lock
 
     method echo_message msg =
+      self#show ();
       let buf = self#buffer in
       self#ignore_insert_text_signal true;
       buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props]
@@ -199,8 +198,10 @@ class console
       self#buffer#insert msg;
       paned#set_position (self#get_max_position - console_height);
       self#misc#grab_focus ()
-    method hide () =
-      paned#set_position self#get_max_position
+    method hide () =  (* ZACK still not sure about the gui, for the moment just
+                       * keep the console persistent *)
+      ()
+(*       paned#set_position self#get_max_position *)
     method toggle () =
       let pos = self#get_position in
       if pos > self#get_max_position - console_height then
@@ -215,33 +216,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