Highlighting of parse errors implemented.

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

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)