Highlighting of parse errors implemented.

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 68b73f36cf9ebd17e13e6d60e213b0939f310dbf..9026e63b34acc4353543d350f63317c808ea4092 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -46,10 +46,8 @@ TODO
 
 
   GUI GRAFICA
+  - cut&paste stile "X": rimane la parte blu e lockata!
   - integrare il famoso logo mancante (anche nell'About dialog)
-  - highlight degli errori di parsing nello script (usando lo sfondo come per la
-    parte lockata di testo, da ripulire quando si modifica il testo o si sposta
-    il punto di esecuzione)
   - invertibilita' dell'inserimento automatico di alias: quando si torna
     su bisognerebbe tornare su di un passo e non fare undo degli alias
     (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
@@ -78,6 +76,7 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
 DONE
+- highlight degli errori di parsing nello script -> CSC
 - quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo
   dalla finestra principale!!! -> CSC
 - sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 066d07cc5af2c0e387748052fbdc3e65bf2e45c4..733d0aab9699e37a5fd59fb9168a96dc674a10af 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -374,8 +374,13 @@ class gui () =
       let locker f = 
         fun () -> 
           lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc
-      in
+          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+      let keep_focus f =
+        fun () ->
+         try
+          f (); source_view#misc#grab_focus ()
+         with
+          exc -> source_view#misc#grab_focus (); raise exc in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -631,19 +636,17 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"));
-        source_view#misc#grab_focus ()
-      in
+          (source_buffer#get_iter_at_mark (`NAME "locked")) in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
-      let advance = locker advance in
-      let retract = locker retract in
-      let top = locker top in
-      let bottom = locker bottom in
-      let jump = locker jump in
+      let advance = locker (keep_focus advance) in
+      let retract = locker (keep_focus retract) in
+      let top = locker (keep_focus top) in
+      let bottom = locker (keep_focus bottom) in
+      let jump = locker (keep_focus jump) in
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4d092ca65e83d44c987c65d272f426349e03ebe3..811b1a858a4b98f873445d76ee4d247d08f8f834 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -354,9 +354,40 @@ let eval_executable guistuff status user_goal parsed_text script ex =
   | TA.Macro (_,mac) ->
       eval_macro guistuff status parsed_text script mac
 
-let rec eval_statement guistuff status user_goal script s =
+let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
+ guistuff status user_goal script s
+=
   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-  let st = GrafiteParser.parse_statement (Stream.of_string s) in
+  let st =
+   try
+    GrafiteParser.parse_statement (Stream.of_string s)
+   with
+    CicNotationParser.Parse_error (floc,err) as exc ->
+     let (x, y) = CicNotationPt.loc_of_floc floc in
+     let x = parsedlen + x in
+     let y = parsedlen + y in
+     let x' = baseoffset + x in
+     let y' = baseoffset + y in
+     let x_iter = buffer#get_iter (`OFFSET x') in
+     let y_iter = buffer#get_iter (`OFFSET y') in
+      buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+     let id = ref None in
+      id :=
+       Some
+        (buffer#connect#changed
+          ~callback:(
+            fun () ->
+             buffer#remove_tag error_tag ~start:buffer#start_iter
+              ~stop:buffer#end_iter;
+             match !id with
+                None -> assert false (* a race condition occurred *)
+              | Some id ->
+                 (new GObj.gobject_ops buffer#as_buffer)#disconnect id));
+      let flocb,floce = floc in
+      let floc =
+       {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y } in
+      raise (CicNotationParser.Parse_error (floc,err))
+  in
   let text_of_loc loc =
     let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
     let parsed_text = safe_substring s 0 parsed_text_length in
@@ -368,7 +399,8 @@ let rec eval_statement guistuff status user_goal script s =
       let remain_len = String.length s - parsed_text_length in
       let s = String.sub s parsed_text_length remain_len in
       let s,len = 
-        eval_statement guistuff status user_goal script s 
+        eval_statement baseoffset (parsedlen + parsed_text_length) error_tag
+         buffer guistuff status user_goal script s 
       in
       (match s with
       | (status, text) :: tl ->
@@ -432,6 +464,7 @@ object (self)
   val locked_mark =
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
+  val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
 
   method locked_mark = locked_mark
 
@@ -443,13 +476,10 @@ object (self)
     let s = match statement with Some s -> s | None -> self#getFuture in
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
     let (entries, parsed_len) = 
-      eval_statement guistuff self#status userGoal self s
+     eval_statement (buffer#get_iter_at_mark (`MARK locked_mark))#offset 0
+      error_tag buffer guistuff self#status userGoal self s
     in
     let (new_statuses, new_statements) = List.split entries in
-(*
-prerr_endline "evalStatement returned";
-List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
-*)
     history <- List.rev new_statuses @ history;
     statements <- List.rev new_statements @ statements;
     let start = buffer#get_iter_at_mark (`MARK locked_mark) in
@@ -459,12 +489,9 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     else
      if new_text <> String.sub s 0 parsed_len then
       begin
-(*       prerr_endline ("new:" ^ new_text); *)
-(*       prerr_endline ("s:" ^ String.sub s 0 parsed_len); *)
        let stop = start#copy#forward_chars parsed_len in
         buffer#delete ~start ~stop;
         buffer#insert ~iter:start new_text;
-(*       prerr_endline "AUTOMATICALLY MODIFIED!!!!!" *)
       end;
     self#moveMark (String.length new_text)