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 =
Common.modname_of_filename status false ocamlfname in
let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
- let status = OcamlExtractionTable.open_file status ~baseuri ocamlfname in
+ let status = OcamlExtraction.open_file status ~baseuri ocamlfname in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
in
let asserted, status =
eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
- let status = OcamlExtractionTable.close_file status in
+ let status = OcamlExtraction.close_file status in
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 s fname true big_bang big_bang_u big_bang_s;
- asserted
+ (*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;
-*))
+*)
+ asserted)
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
let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
let asserted,children_bad =
List.fold_left
- (fun (asserted,b) mapath ->
- let asserted,b1 =
- assert_ng ~already_included ~compiling ~asserted ~include_paths
- mapath
+ (fun (asserted,b) mapath ->
+ let asserted,b1 =
+ try
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mapath
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ asserted, true
in
asserted, b || b1
|| let _,baseuri,_,_ =