X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;h=3757b177f1706dc3fc290c8f402a20af3a51dbe0;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=9c86679bc420789579639adda15aa29d6676e615;hpb=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;p=helm.git

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 9c86679bc..3757b177f 100644
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -135,50 +135,61 @@ let baseuri_of_script ~include_paths fname =
 let rec get_ast status ~compiling ~asserted ~include_paths strm = 
   match GrafiteParser.parse_statement status strm with
      (GrafiteAst.Executable
-       (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
+       (loc,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
      ->
        let already_included = NCicLibrary.get_transitively_included status in
        let asserted,_ =
         assert_ng ~already_included ~compiling ~asserted ~include_paths
-         mafilename
+         ?uid:status#user mafilename
        in
         asserted,cmd
    | cmd -> asserted,cmd
 
 and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status =
-  let asserted,stop,status = 
+ let rec loop asserted status str =
+  let asserted,stop,status,str = 
    try
      let cont =
        try Some (get_ast status ~compiling ~asserted ~include_paths str)
        with End_of_file -> None in
      match cont with
-     | None -> asserted, true, status
+     | None -> asserted, true, status, str
      | Some (asserted,ast) ->
         cb status ast;
         let status =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
         in
-         asserted, false, status
+        let str =
+         match ast with
+            (GrafiteAst.Executable
+              (_,GrafiteAst.NCommand
+                (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+              GrafiteParser.parsable_statement status
+               (GrafiteParser.strm_of_parsable str)
+          | _ -> str
+        in
+         asserted, false, status, str
    with exn when not matita_debug ->
+     (* prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); *)
      raise (EnrichedWithStatus (exn, status))
   in
-  if stop then asserted,status else loop asserted status
+  if stop then asserted,status else loop asserted status str
  in
-  loop asserted status
+  loop asserted status str
 
-and compile ~compiling ~asserted ~include_paths ~outch fname =
+and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
+  let matita_debug = true in
   let root,baseuri,fname,_tgt = 
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
   (* FIXME: currently hardcoded to single user mode *)
-  let status = new status None baseuri in
+  let status = new status uid baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -211,6 +222,7 @@ and compile ~compiling ~asserted ~include_paths ~outch fname =
         (Filename.dirname 
           (Http_getter.filename ~local:true ~writable:true (baseuri ^
           "foo.con")));
+    prerr_endline ("trying to compile " ^ fname); 
     let buf =
      GrafiteParser.parsable_statement status
       (Ulexing.from_utf8_channel (open_in fname))
@@ -221,6 +233,7 @@ and compile ~compiling ~asserted ~include_paths ~outch fname =
     in
     let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+    prerr_endline ("end compile of " ^ fname); 
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
@@ -237,10 +250,11 @@ and compile ~compiling ~asserted ~include_paths ~outch fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times fname true big_bang big_bang_u big_bang_s;
-     (* 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 
@@ -263,6 +277,9 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
    let baseuri = NUri.uri_of_string baseuri in
    let ngtime_of baseuri =
     let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
+    let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in
+    (* prerr_endline ("uid = " ^ uid);
+    prerr_endline ("ngpath = " ^ ngpath); *)
     try
      Some (Unix.stat ngpath).Unix.st_mtime
     with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
@@ -280,7 +297,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
           (fun (asserted,b) mapath ->
             let asserted,b1 =
               assert_ng ~already_included ~compiling ~asserted ~include_paths
-               mapath
+                ?uid mapath
             in
              asserted, b || b1
               || let _,baseuri,_,_ =
@@ -294,6 +311,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
          asserted, children_bad || matime > ngtime
      | None -> asserted,true
    in
+    (* prerr_endline ("asserted = " ^ (String.concat "," asserted)); *)
     if not to_be_compiled then fullmapath::asserted,false
     else
      if List.mem baseuri already_included then
@@ -305,12 +323,40 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
         | None -> open_out (fullmapath ^ ".mad"), true
         | Some c -> c, false
       in
-      let asserted = compile ~compiling ~asserted ~include_paths ~outch fullmapath in
+      (* prerr_endline ("compiling " ^ fullmapath); *)
+      let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
        if is_file_ch then close_out outch;
        fullmapath::asserted,true
   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)