X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaConsole.ml;h=3d40e949ee46ae156abe5e34625c7dbac8346fc2;hb=f38e8fafcf040258b54b4032562753a876a8a94e;hp=222055e6539a59b8b9ecfed8bf3434d746bcb936;hpb=e35ec00b1be70e4b064b74a49735b37b5e719e5b;p=helm.git

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 222055e65..3d40e949e 100644
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -27,10 +27,13 @@ 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 ]
 let error_props = [ `WEIGHT `BOLD ]
@@ -92,6 +95,7 @@ class console
     val history = new history BuildTimeConf.console_history_size
 
     val mutable handle_position = 450
+    val mutable last_phrase = ""
 
     initializer
       let buf = self#buffer in
@@ -107,13 +111,15 @@ class console
           (Pcre.pmatch ~rex:trailing_NL_RE text)
         then
           let inserted_text =
-            buf#get_text
-              ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
-              ~stop:buf#end_iter ()
+            MatitaMisc.strip_trailing_blanks
+              (buf#get_text
+                ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+                ~stop:buf#end_iter ())
           in
           let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
           if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
             self#lock;
+            last_phrase <- inserted_text;
             self#invoke_callback inserted_text;
             self#echo_prompt ()
           end));
@@ -141,15 +147,9 @@ class console
       buf#insert ~iter:buf#end_iter phrase
 
     method private invoke_callback phrase =
-      history#add (* do not push trailing phrase separator *)
-        (String.sub phrase 0
-          (String.length phrase - String.length _phrase_sep));
-      if _callback phrase then begin
-        self#hide ();
-        self#clear ()
-        (* else callback encountered troubles, don't hide console which
-        probably contains error message *)
-      end
+      history#add phrase;
+      let (success, hide) = _callback phrase in
+      if hide then self#hide ()
 
     method clear () =
       let buf = self#buffer in
@@ -170,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]
@@ -197,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
@@ -213,18 +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
-      | 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
 
@@ -241,3 +254,4 @@ let console
   in
   new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
 
+(* vim: set encoding=utf8: *)