let out = ref ignore
let set_callback f = out := f
+
let slash_n_RE = Pcre.regexp "\\n" ;;
let pp_ast_statement grafite_status stm =
LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc
;;
+let dump f =
+ let module G = GrafiteAst in
+ let module L = LexiconAst in
+ let module H = HExtlib in
+ Helm_registry.set_bool "matita.moo" false;
+ let floc = H.dummy_floc in
+ let nl_ast = G.Comment (floc, G.Note (floc, "")) in
+ let och = open_out f in
+ let out_comment och s =
+ let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in
+ Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
+ in
+ let out_line_comment och s =
+ let l = 70 - String.length s in
+ let s = Printf.sprintf " %s %s" s (String.make l '*') in
+ out_comment och s
+ in
+ let out_preamble och (path, lines) =
+ let ich = open_in path in
+ let rec print i =
+ if i > 0 then
+ let s = input_line ich in
+ begin Printf.fprintf och "%s\n" s; print (pred i) end
+ in
+ print lines;
+ out_line_comment och "This file was automatically generated: do not edit"
+ in
+ let pp_ast_statement st =
+ GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ ~lazy_term_pp:CicNotationPp.pp_term
+ ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
+ in
+ let nl () = output_string och (pp_ast_statement nl_ast) in
+ let rt_base_dir = Filename.dirname Sys.argv.(0) in
+ let path = Filename.concat rt_base_dir "matita.ma.templ" in
+ let lines = 14 in
+ out_preamble och (path, lines);
+ let grafite_parser_cb fname =
+ let ast = G.Executable
+ (floc, G.Command (floc, G.Include (floc, fname))) in
+ output_string och (pp_ast_statement ast); nl (); nl ()
+ in
+ let matita_engine_cb = function
+ | G.Executable (_, G.Macro (_, G.Inline _))
+ | G.Executable (_, G.Command (_, G.Include _)) -> ()
+ | ast ->
+ output_string och (pp_ast_statement ast); nl (); nl ()
+ in
+ let matitac_lib_cb = output_string och in
+ GrafiteParser.set_callback grafite_parser_cb;
+ MatitaEngine.set_callback matita_engine_cb;
+ set_callback matitac_lib_cb;
+ fun x ->
+ close_out och;
+ GrafiteParser.set_callback ignore;
+ MatitaEngine.set_callback ignore;
+ set_callback ignore; x
+;;
+
let get_macro_context = function
| Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
| Some status ->
;;
let activate_extraction baseuri fname =
- if false then
+ 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
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
LexiconSync.time_travel
~present:lexicon_status ~past:initial_lexicon_status;
clean_exit baseuri false
- | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) ->
+ | 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;
+ | Sys.Break when not matita_debug ->
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;
+ | exn when not matita_debug ->
HLog.error
("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn));
pp_times fname false big_bang big_bang_u big_bang_s;
let root,baseuri,_,_ =
Librarian.baseuri_of_script ~include_paths mafile
in
- Some root, LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
+ 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 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 build = compile;;
+ 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 load_deps_file = Librarian.load_deps_file;;
+ let load_deps_file = Librarian.load_deps_file
end
projects / helm.git / blobdiff