grafite parser updated

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

diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml
index 69859470fb6e6500ddae95b728af85541b497381..6d703b556b3706abeb94281d1c44a0af0dd1d3a4 100644 (file)
--- a/matitaB/matita/matitaScript.ml
+++ b/matitaB/matita/matitaScript.ml
@@ -180,12 +180,12 @@ and eval_statement include_paths (buffer : GText.buffer) status script
     | `Ast (st, text) -> st, text
   in
   let text_of_loc floc = 
-    let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
+    let nonskipped_txt,_ = HExtlib.utf8_parsed_text unparsed_text floc in
     let start, stop = HExtlib.loc_of_floc floc in 
     let floc = HExtlib.floc_of_loc (0, start) in
-    let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
+    let skipped_txt,_ = HExtlib.utf8_parsed_text unparsed_text floc in
     let floc = HExtlib.floc_of_loc (0, stop) in
-    let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
+    let txt,len = HExtlib.utf8_parsed_text unparsed_text floc in
     txt,nonskipped_txt,skipped_txt,len
   in 
   match st with
@@ -209,10 +209,10 @@ and eval_statement include_paths (buffer : GText.buffer) status script
           HExtlib.Localized (floc, exn) ->
            HExtlib.raise_localized_exception 
              ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
-        | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+       (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
            raise
             (MultiPassDisambiguator.DisambiguationError
-              (offset+parsed_text_length, errorll))
+              (offset+parsed_text_length, errorll)) *)
       in
       assert (text=""); (* no macros inside comments, please! *)
       let st,text = s in
@@ -1023,29 +1023,7 @@ object (self)
     | _::[] -> true
     | _ -> false
 
-  method eos = 
-    let rec is_there_only_comments status s = 
-      if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      let strm =
-       GrafiteParser.parsable_statement status
-        (Ulexing.from_utf8_string s)in
-      match GrafiteParser.parse_statement status strm with
-      | GrafiteAst.Comment (loc,_) -> 
-          let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
-          (* CSC: why +1 in the following lines ???? *)
-          let parsed_text_length = parsed_text_length + 1 in
-          let remain_len = String.length s - parsed_text_length in
-          let next = String.sub s parsed_text_length remain_len in
-          is_there_only_comments status next
-      | GrafiteAst.Executable _ -> false
-    in
-    try is_there_only_comments self#status self#getFuture
-    with 
-    | NCicLibrary.IncludedFileNotCompiled _
-    | HExtlib.Localized _
-    | CicNotationParser.Parse_error _ -> false
-    | Margin | End_of_file -> true
-    | Invalid_argument "Array.make" -> false
+  method eos = MatitaEngine.eos self#status self#getFuture 
 
   (* debug *)
   method dump () =