X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;h=83eb235fb82350d3dd2baa613580d73195c72203;hb=3b88d3315fe9a716d32cc51adb2e2d151cd447e8;hp=aa271b2a1ca948b69ae67c3c008fd871e479fb59;hpb=d8ae533d041cb600993ab2957111c105b6ded21d;p=helm.git

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index aa271b2a1..83eb235fb 100644
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -240,7 +240,9 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
      (* XXX: update script -- currently to stdout *)
      let origbuf = Ulexing.from_utf8_channel (open_in fname) in
      let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
-     ignore (SmallLexer.mk_small_printer interpr outch origbuf);
+     let outstr = ref "" in
+     ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
+     Printf.fprintf outch "%s" !outstr;
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
@@ -316,6 +318,33 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
   end
 ;;
 
+let eos status s =
+  let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" in      
+  let rec is_there_only_comments status s = 
+  if Pcre.pmatch ~rex:only_dust_RE s then raise End_of_file;
+  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 = HExtlib.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 status s
+  with 
+  | NCicLibrary.IncludedFileNotCompiled _
+  | HExtlib.Localized _
+  | CicNotationParser.Parse_error _ -> false
+  | End_of_file -> true
+  | Invalid_argument "Array.make" -> false
+;;
+
+
 let assert_ng ~include_paths ?outch mapath =
  snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
   ?outch mapath)