prerr_endline (sprintf "dumping MathML to %s ..." fname);
flush stdout;
let oc = open_out fname in
- let markup = CicNotationPres.render id_to_uri t in
+ let markup =
+ CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri id_to_uri)t in
let xml_stream = CicNotationPres.print_xml markup in
Xml.pp_to_outchan xml_stream oc;
close_out oc
let module G = GrafiteAst in
let status =
ref
- (CicNotation2.load_notation
+ (CicNotation2.load_notation (new LexiconEngine.status)
~include_paths:[] (Helm_registry.get "notation.core_file"))
in
try
prerr_endline
("Unsupported statement: " ^
GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
~term_pp:CicNotationPp.pp_term
~lazy_term_pp:(fun _ -> "_lazy_term_here_")
~obj_pp:(fun _ -> "_obj_here_")
(!char_count + x) (!char_count + y) msg)
| exn ->
prerr_endline
- (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
+ (sprintf "TestParser: Uncaught exception: %s" (Printexc.to_string exn))
done
with End_of_file -> ()