X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaScript.ml;h=6d703b556b3706abeb94281d1c44a0af0dd1d3a4;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=5b794a6d830b8d9c0c1690faa9578388c94699ca;hpb=42680d47c033d751738fd0f84af7b45b2a91a5b8;p=helm.git

diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml
index 5b794a6d8..6d703b556 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
@@ -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
@@ -245,7 +245,8 @@ let source_buffer = source_view#source_buffer in
 let similarsymbols_tag_name = "similarsymbolos" in
 let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
- let status = new MatitaEngine.status baseuri in
+(* FIXME : currently hard coded to single user mode *)
+ let status = new MatitaEngine.status None baseuri in
  (match current with
      Some current ->
       NCicLibrary.time_travel status;
@@ -1022,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 () =