+
+(* term xml printing ********************************************************)
+
+let id frm a =
+ let f s = function
+ | true -> F.fprintf frm " name=%S" s
+ | false -> F.fprintf frm " name=%S" ("^" ^ s)
+ in
+ B.name C.start f a
+
+let rec exp_term c frm = function
+ | B.Sort (a, l) ->
+ let a =
+ let err _ = a in
+ let f s = B.Name (true, s) :: a in
+ H.get_sort err f l
+ in
+ F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) id a
+ | B.LRef (a, i) ->
+ let a =
+ let err _ = a in
+ let f n r = B.Name (r, n) :: a in
+ let f _ b = attrs_of_binder (B.name err f) b in
+ B.get err f c i
+ in
+ F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) id a
+ | B.GRef (a, u) ->
+ let a = B.Name (true, U.name_of_uri u) :: a in
+ F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) id a
+ | B.Cast (a, w, t) ->
+ F.fprintf frm "<Cast%a>%a</Cast>@,%a" id a (exp_boxed c) w (exp_term c) t
+ | B.Appl (a, v, t) ->
+ F.fprintf frm "<Appl%a>%a</Appl>@,%a" id a (exp_boxed c) v (exp_term c) t
+ | B.Bind (b, t) ->
+ let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in
+ let f b = B.push (f b) c b in
+ rename_bind f c b
+
+and exp_boxed c frm t =
+ F.fprintf frm "@,@[<v3> %a@]@," (exp_term c) t
+
+and exp_bind c frm = function
+ | B.Abst (a, w) ->
+ F.fprintf frm "<Abst%a>%a</Abst>" id a (exp_boxed c) w
+ | B.Abbr (a, v) ->
+ F.fprintf frm "<Abbr%a/>%a</Abbr>" id a (exp_boxed c) v
+ | B.Void a ->
+ F.fprintf frm "<Void%a/>" id a
+
+let exp_entry c frm = function
+ | _, u, B.Abst (a, w) ->
+ let str = U.string_of_uri u in
+ let a = B.Name (true, U.name_of_uri u) :: a in
+ F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str id a (exp_boxed c) w
+ | _, u, B.Abbr (a, v) ->
+ let str = U.string_of_uri u in
+ let a = B.Name (true, U.name_of_uri u) :: a in
+ F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str id a (exp_boxed c) v
+ | _, u, B.Void a ->
+ let str = U.string_of_uri u in
+ let a = B.Name (true, U.name_of_uri u) :: a in
+ F.fprintf frm "<VOID uri=%S%a/>" str id a
+
+let export_entry frm entry =
+ F.fprintf frm "@,@[<v3> %a@]@," (exp_entry B.empty_lenv) entry