summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
6640fe3)
This is implemented imperatively for now. It should go into a status.
if Http_getter_storage.is_read_only baseuri then assert false;
(* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
let status = new status baseuri in
if Http_getter_storage.is_read_only baseuri then assert false;
(* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
let status = new status baseuri in
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
let ocamldirname = Filename.dirname fname in
let ocamlfname = Filename.chop_extension (Filename.basename fname) in
let status,ocamlfname =
let ocamldirname = Filename.dirname fname in
let ocamlfname = Filename.chop_extension (Filename.basename fname) in
let status,ocamlfname =
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
pp_times s 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 s fname true big_bang big_bang_u big_bang_s;
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| exn when not matita_debug ->
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
* *)
with
(* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
| exn when not matita_debug ->
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
* *)
+ (*CSC: bad, one imperative bit is still there!
+ to be moved into functional status *)
+ NCicMetaSubst.pushmaxmeta ();
pp_times s fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri exn
pp_times s fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri exn