X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matitaB%2Fmatita%2FmatitaScript.ml;h=aa51b36a0cc0a3f1f1d6b7a5d17622b2c7d40dfa;hb=71c124b4f171059ec3d29d5e53079000773ec851;hp=69859470fb6e6500ddae95b728af85541b497381;hpb=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;p=helm.git

diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml
index 69859470f..aa51b36a0 100644
--- 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
@@ -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 () =