CicNotation2.load_notation ~include_paths:[]
BuildTimeConf.core_notation_script
in
- let initial_lexicon_status = lexicon_status in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
with MatitaEngine.EnrichedWithLexiconStatus
(GrafiteEngine.Macro (floc, f), lex_status) as exn ->
match f (get_macro_context (Some grafite_status)) with
- | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+ | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
let str =
- ApplyTransformation.txt_of_inline_macro style suri prefix
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex") in
+ ApplyTransformation.txt_of_inline_macro style prefix suri
+ ?flavour
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ in
!out str;
aux_for_dump x
|_-> raise exn
(HLog.error
"there are still incomplete proofs at the end of the script";
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)
else
(if not (Helm_registry.get_bool "matita.moo" &&
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
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;
+(* 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 when not matita_debug ->
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 root,baseuri,_,_ =
Librarian.baseuri_of_script ~include_paths mafile
in
- let obj =
- if Filename.check_suffix mafile ".mma" then
- Filename.chop_suffix mafile ".mma" ^ ".ma"
- else
- LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- in
- Some root, obj
- with Librarian.NoRootFor x -> None, ""
+ let obj_writeable, obj_read_only =
+ if Filename.check_suffix mafile ".mma" then
+ Filename.chop_suffix mafile ".mma" ^ ".ma",
+ Filename.chop_suffix mafile ".mma" ^ ".ma"
+ else
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ Some root, obj_writeable, obj_read_only
+ with Librarian.NoRootFor x -> None, "", ""
+ ;;
let mtime_of_source_object s =
try Some (Unix.stat s).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+ ;;
let mtime_of_target_object s =
try Some (Unix.stat s).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+ ;;
let build options fname =
- if Filename.check_suffix fname ".mma" then
- let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
- let atexit = dump generated in
- let res = compile options fname in
- atexit res
- else
- compile options fname
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let compile opts fname =
+ try
+ GrafiteSync.push ();
+ GrafiteParser.push ();
+ let rc = compile opts fname in
+ GrafiteParser.pop ();
+ GrafiteSync.pop ();
+ rc
+ with
+ | Sys.Break ->
+ GrafiteParser.pop ();
+ GrafiteSync.pop ();
+ false
+ | exn when not matita_debug ->
+ HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
+ assert false
+ in
+ if Filename.check_suffix fname ".mma" then
+ let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
+ let atexit = dump generated in
+ let res = compile options fname in
+ let r = atexit res in
+ if r then r else begin
+ Sys.remove generated;
+ Printf.printf "rm %s\n" generated; flush stdout; r
+ end
+ else
+ compile options fname
+ ;;
- let load_deps_file = Librarian.load_deps_file
+ let load_deps_file = Librarian.load_deps_file;;
end