+ (if not (Helm_registry.get_bool "matita.moo" &&
+ Filename.check_suffix fname ".mma") then begin
+ (* FG: we do not generate .moo when dumping .mma files *)
+ GrafiteMarshal.save_moo moo_fname moo_content_rev;
+ LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+ end;
+ let tm = Unix.gmtime elapsed in
+ let sec = string_of_int tm.Unix.tm_sec ^ "''" in
+ let min =
+ if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else ""
+ in
+ let hou =
+ if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else ""
+ in
+ 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;
+ LexiconSync.time_travel
+ ~present:lexicon_status ~past:initial_lexicon_status;
+ true)
+ with
+ (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
+ | AttemptToInsertAnAlias lexicon_status ->
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ LexiconSync.time_travel
+ ~present:lexicon_status ~past:initial_lexicon_status;
+ clean_exit baseuri false
+ | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) as exn' ->
+ (match exn with
+ | Sys.Break -> HLog.error "user break!"
+ | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+ let (x, y) = HExtlib.loc_of_floc floc in
+ HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
+ | exn when matita_debug -> raise exn'
+ | exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
+ LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri false
+ | Sys.Break as exn ->
+ if matita_debug then raise exn;
+ HLog.error "user break!";
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri false
+ | exn ->
+ if matita_debug then raise exn;
+ HLog.error
+ ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
+ pp_times fname false big_bang big_bang_u big_bang_s;
+ clean_exit baseuri false
+
+module F =
+ struct
+ type source_object = string
+ type target_object = string
+ let string_of_source_object s = s;;
+ let string_of_target_object s = s;;
+
+ let is_readonly_buri_of opts file =
+ let buri = List.assoc "baseuri" opts in
+ Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file)
+
+ let root_and_target_of opts mafile =
+ try
+ let include_paths = get_include_paths opts in
+ let root,baseuri,_,_ =
+ Librarian.baseuri_of_script ~include_paths mafile
+ in
+ Some root, LibraryMisc.obj_file_of_baseuri