+
+let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name =
+ let suri =
+ if Librarian.is_uri name then name else
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes"
+ in
+ let _, baseuri, _, _ =
+ Librarian.baseuri_of_script ~include_paths name
+ in
+ baseuri ^ "/"
+ in
+ txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri
+
+(****************************************************************************)
+(* procedural_txt_of_cic_term *)
+
+let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
+ let term, _info = PO.optimize_term context term in
+ let annterm, ids_to_inner_sorts, ids_to_inner_types =
+ try Cic2acic.acic_term_of_cic_term context term
+ with e ->
+ let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
+ failwith msg
+ in
+ let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
+ let lazy_term_pp = term_pp in
+ let obj_pp = CicNotationPp.pp_obj term_pp in
+ let aux = GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
+ let script =
+ Acic2Procedural.procedural_of_acic_term
+ ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm
+ in
+ String.concat "" (List.map aux script)
+;;
+
+(****************************************************************************)
+
+let txt_of_macro ~map_unicode_to_tex metasenv context m =
+ GrafiteAstPp.pp_macro
+ ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context)
+ ~lazy_term_pp:(fun (f : Cic.lazy_term) ->
+ let t,metasenv,_ = f context metasenv CicUniv.empty_ugraph in
+ txt_of_cic_term ~map_unicode_to_tex 80 metasenv context t)
+ m
+;;
+
+