New implementation for localized exceptions.

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 34e0408c598f281aa0d6bee4417bc3ad5493e407..4413f9b8a3bbc0726c752a1cdd53fcafe564df71 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -372,49 +372,18 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
   | TA.Macro (_,mac) ->
       eval_macro guistuff status user_goal unparsed_text parsed_text script mac
 
-let parse_statement baseoffset parsedlen ?error_tag (buffer: GText.buffer) text 
-=
-  try
-    GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
-  with CicNotationParser.Parse_error (floc, err) as exn ->
-    match error_tag with
-    | None -> raise exn
-    | Some error_tag ->
-        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
-        buffer#place_cursor (buffer#get_iter (`OFFSET x'));
-        raise (CicNotationParser.Parse_error (floc, err))
-
-let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
- guistuff status user_goal script statement
+let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
+ script statement
 =
   let st, unparsed_text =
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
-        parse_statement baseoffset parsedlen ~error_tag buffer text, text
+        GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text
     | `Ast (st, text) -> st, text
   in
   let text_of_loc loc =
-    let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
+    let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
     let parsed_text = safe_substring unparsed_text 0 parsed_text_length in
     parsed_text, parsed_text_length
   in
@@ -424,8 +393,12 @@ let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
       let remain_len = String.length unparsed_text - parsed_text_length in
       let s = String.sub unparsed_text parsed_text_length remain_len in
       let s,len = 
-        eval_statement baseoffset (parsedlen + parsed_text_length) error_tag
-         buffer guistuff status user_goal script (`Raw s)
+       try
+        eval_statement buffer guistuff status user_goal script
+         (`Raw s)
+       with HExtlib.Localized (floc, exn) ->
+        HExtlib.raise_localized_exception
+         ~offset:parsed_text_length floc exn
       in
       (match s with
       | (status, (text, ast)) :: tl ->
@@ -494,6 +467,7 @@ object (self)
 
   method locked_mark = locked_mark
   method locked_tag = locked_tag
+  method error_tag = error_tag
 
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)
@@ -501,10 +475,8 @@ object (self)
 
   method private _advance ?statement () =
     let rec aux st =
-      let baseoffset = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in
       let (entries, parsed_len) = 
-        eval_statement baseoffset 0 error_tag buffer guistuff self#status
-          userGoal self st
+        eval_statement buffer guistuff self#status userGoal self st
       in
       let (new_statuses, new_statements, new_asts) =
         let statuses, statements = List.split entries in
@@ -534,7 +506,7 @@ object (self)
           in
           let text = self#getFuture in
           (try
-            (match parse_statement baseoffset 0 ?error_tag:None buffer text with
+            (match parse_statement baseoffset 0 buffer text with
             | TA.Executable (loc, TA.Tactical (_, tac, None)) as st
               when GrafiteAst.is_punctuation tac ->
                 let len = snd (CicNotationPt.loc_of_floc loc) in
@@ -774,7 +746,7 @@ object (self)
       let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in
       match st with
       | GrafiteAst.Comment (loc,_)-> 
-          let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
+          let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_and_executable next