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,_ =
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 ?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;
(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))
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)
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
let outstr = ref "" 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);
+ (* 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
asserted, children_bad || matime > ngtime
| None -> asserted,true
in
- prerr_endline ("asserted = " ^ (String.concat "," asserted));
+ (* 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
- prerr_endline ("compiling " ^ fullmapath);
+ (* 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