String.sub s lenp (lens-lenp)
;;
-let print_string =
+let print_string =
let indent = ref 0 in
let print_string ~right_justify s =
let ss =
match right_justify with
None -> ""
| Some (ss,len_ss) ->
- String.make (80 - !indent - len_ss - String.length s) ' ' ^ ss
+ let i = 80 - !indent - len_ss - String.length s in
+ if i > 0 then String.make i ' ' ^ ss else ss
in
+ assert (!indent >=0);
print_string (String.make !indent ' ' ^ s ^ ss) in
fun enter ?right_justify s ->
if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
;;
-let activate_extraction baseuri fname =
- ()
- (* MATITA 1.0
- if Helm_registry.get_bool "matita.extract" then
- let mangled_baseuri =
- let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
- let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
- String.uncapitalize baseuri in
- let f =
- open_out
- (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
- LibrarySync.add_object_declaration_hook
- (fun ~add_obj ~add_coercion _ obj ->
- output_string f (CicExportation.ppobj baseuri obj);
- flush f; []);
- *)
-;;
-
-
let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
let baseuri = status#baseuri in
let new_aliases,new_status =
GrafiteDisambiguate.eval_with_new_aliases status
(fun status ->
+ let time0 = Unix.gettimeofday () in
+ let status =
GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
- (text,prefix_len,ast)) in
+ (text,prefix_len,ast) in
+ let time1 = Unix.gettimeofday () in
+ HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s");
+ status
+ ) in
let _,intermediate_states =
List.fold_left
(fun (status,acc) (k,value) ->
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
- activate_extraction baseuri fname ;
(* 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 = 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 ()
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
else pp_ast_statement
in
- let asserted, times, status =
+ let asserted, status =
eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb 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,_,_ =