snapshot

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

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 222055e6539a59b8b9ecfed8bf3434d746bcb936..889d8e2d80244eb0aa23062347f4875819a6c401 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -31,6 +31,7 @@ open MatitaTypes
 let default_prompt = ""
 let default_phrase_sep = "."
 let default_callback = fun (phrase: string) -> true
+let bullet = "∙"
 
 let message_props = [ `STYLE `ITALIC ]
 let error_props = [ `WEIGHT `BOLD ]
@@ -92,6 +93,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 +109,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 +145,13 @@ 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));
+      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 *)
-      end
 
     method clear () =
       let buf = self#buffer in
@@ -221,6 +223,21 @@ class console
       | 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));
@@ -241,3 +258,4 @@ let console
   in
   new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
 
+(* vim: set encoding=utf8: *)