let slash_n_RE = Pcre.regexp "\\n" ;;
let pp_ast_statement grafite_status stm =
- let stm = GrafiteAstPp.pp_statement
+ let stm = GrafiteAstPp.pp_statement stm
~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
- ~term_pp:NotationPp.pp_term
- ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj
- NotationPp.pp_term) stm
in
let stm = Pcre.replace ~rex:slash_n_RE stm in
let stm =
let floc = H.dummy_floc in
let nl_ast = G.Comment (floc, G.Note (floc, "")) in
let pp_statement stm =
- GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
+ GrafiteAstPp.pp_statement stm
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- ~lazy_term_pp:NotationPp.pp_term
- ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm
in
let pp_lexicon = LexiconAstPp.pp_command in
let och = open_out f in
let nl () = output_string och (pp_statement nl_ast) in
MatitaMisc.out_preamble och;
let grafite_parser_cb = function
- | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
+ | G.Executable (loc, G.Command (_, G.Include (_,_))) -> ()
| stm ->
output_string och (pp_statement stm); nl (); nl ()
in
BuildTimeConf.core_notation_script
in
atstart (); (* FG: do not invoke before loading the core notation script *)
- let grafite_status = GrafiteSync.init lexicon_status baseuri in
+ let grafite_status =
+ (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
let matita_debug = Helm_registry.get_bool "matita.debug" in
let compile atstart opts fname =
try
- GrafiteSync.push ();
GrafiteParser.push ();
let rc = compile atstart 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));