let rec get_ast status ~compiling ~asserted ~include_paths strm =
match GrafiteParser.parse_statement status strm with
(GrafiteAst.Executable
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
match cont with
| None -> asserted, true, status, str
| Some (asserted,ast) ->
match cont with
| None -> asserted, true, status, str
| Some (asserted,ast) ->
in
asserted, false, status, str
with exn when not matita_debug ->
in
asserted, false, status, str
with exn when not matita_debug ->
raise (EnrichedWithStatus (exn, status))
in
if stop then asserted,status else loop asserted status str
raise (EnrichedWithStatus (exn, status))
in
if stop then asserted,status else loop asserted status str
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;
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;
let origbuf = Ulexing.from_utf8_channel (open_in fname) in
let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
let outstr = ref "" in
ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
Printf.fprintf outch "%s" !outstr;
let origbuf = Ulexing.from_utf8_channel (open_in fname) in
let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
let outstr = ref "" in
ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
Printf.fprintf outch "%s" !outstr;
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
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
try
Some (Unix.stat ngpath).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
try
Some (Unix.stat ngpath).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
if not to_be_compiled then fullmapath::asserted,false
else
if List.mem baseuri already_included then
if not to_be_compiled then fullmapath::asserted,false
else
if List.mem baseuri already_included then
let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
if is_file_ch then close_out outch;
fullmapath::asserted,true
let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
if is_file_ch then close_out outch;
fullmapath::asserted,true