open Printf
-module Ast = CicNotationPt
+module Ast = NotationPt
module Mpres = Mpresentation
type mathml_markup = boxml_markup Mpres.mpres
let kind, spacing, indent = spec in
let dress children =
if spacing then
- CicNotationUtil.dress small_skip children
+ NotationUtil.dress small_skip children
else
children
in
BoxPp.render_to_string (function x::_->x|_->assert false)
~map_unicode_to_tex:false 80 t);*)t)
-let lookup_uri ids_to_uris id =
- try
- let uri = Hashtbl.find ids_to_uris id in
- Some (UriManager.string_of_uri uri)
- with Not_found -> None
-;;
-
-let render ~lookup_uri ?(prec=(-1)) =
+let render status ~lookup_uri ?(prec=(-1)) =
let module A = Ast in
let module P = Mpresentation in
(* let use_unicode = true in *)
let substs' =
box_of mathonly (A.H, false, false) []
(open_brace
- :: (CicNotationUtil.dress semicolon
+ :: (NotationUtil.dress semicolon
(List.map
(fun (name, t) ->
box_of mathonly (A.H, false, false) [] [
let local_context l =
box_of mathonly (A.H, false, false) []
([ Mpres.Mtext ([], "[") ] @
- (CicNotationUtil.dress (Mpres.Mtext ([], ";"))
+ (NotationUtil.dress (Mpres.Mtext ([], ";"))
(List.map
(function
| None -> Mpres.Mtext ([], "_")
| A.Magic _
| A.Variable _ -> assert false (* should have been instantiated *)
| t ->
- prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t);
+ prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t);
assert false
and aux_attributes xmlattrs mathonly xref prec t =
let reset = ref false in
then ((*prerr_endline "reset";*)t')
else add_parens child_prec prec t')
in
-(* prerr_endline (CicNotationPp.pp_term t); *)
+(* prerr_endline (NotationPp.pp_term t); *)
aux_attribute t
and aux_literal xmlattrs xref prec l =
let attrs = make_href xmlattrs xref in
| A.Box ((_, spacing, _) as kind, terms) ->
let children =
aux_children mathonly spacing xref prec
- (CicNotationUtil.ungroup terms)
+ (NotationUtil.ungroup terms)
in
box_of mathonly kind attrs children
| A.Mstyle (l,terms) ->
(List.map (fun (k,v) -> None,k,v) l,
box_of mathonly (A.H, false, false) attrs
(aux_children mathonly false xref prec
- (CicNotationUtil.ungroup terms)))
+ (NotationUtil.ungroup terms)))
| A.Mpadded (l,terms) ->
Mpres.Mpadded
(List.map (fun (k,v) -> None,k,v) l,
box_of mathonly (A.H, false, false) attrs
(aux_children mathonly false xref prec
- (CicNotationUtil.ungroup terms)))
+ (NotationUtil.ungroup terms)))
| A.Maction alternatives ->
toggle_action (List.map invoke_reinit alternatives)
| A.Group terms ->
let children =
aux_children mathonly false xref prec
- (CicNotationUtil.ungroup terms)
+ (NotationUtil.ungroup terms)
in
box_of mathonly (A.H, false, false) attrs children
| A.Break -> assert false (* TODO? *)