cb status ast;
let status =
eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
in
asserted, false, status
with exn when not matita_debug ->
cb status ast;
let status =
eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
in
asserted, false, status
with exn when not matita_debug ->
raise (EnrichedWithStatus (exn, status))
in
if stop then asserted,status else loop asserted status
raise (EnrichedWithStatus (exn, status))
in
if stop then asserted,status else loop asserted status
if List.mem fname compiling then raise (CircularDependency fname);
let compiling = fname::compiling in
let matita_debug = Helm_registry.get_bool "matita.debug" in
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 root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
let elapsed = Unix.time () -. time in
(if Helm_registry.get_bool "matita.moo" then begin
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
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;
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;