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
in
loop asserted status
-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
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 ()
(* 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
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
(fun (asserted,b) mapath ->
let asserted,b1 =
assert_ng ~already_included ~compiling ~asserted ~include_paths
- mapath
+ ?uid mapath
in
asserted, b || b1
|| let _,baseuri,_,_ =
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
| 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