+
+(* term xml printing ********************************************************)
+
+let rec exp_term e t out tab = match t with
+ | B.Sort (a, l) ->
+ let a =
+ let err _ = a in
+ let f s = Y.Name (s, true) :: a in
+ H.string_of_sort err f l
+ in
+ let attrs = [X.position l; X.name a] in
+ X.tag X.sort attrs out tab
+ | B.LRef (a, i) ->
+ let a =
+ let err _ = a in
+ let f n r = Y.Name (n, r) :: a in
+ let _, _, a, b = B.get e i in
+ Y.name err f a
+ in
+ let attrs = [X.position i; X.name a] in
+ X.tag X.lref attrs out tab
+ | B.GRef (a, n) ->
+ let a = Y.Name (U.name_of_uri n, true) :: a in
+ let attrs = [X.uri n; X.name a] in
+ X.tag X.gref attrs out tab
+ | B.Cast (a, u, t) ->
+ let attrs = [] in
+ X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+ exp_term e t out tab
+ | B.Appl (a, v, t) ->
+ let attrs = [] in
+ X.tag X.appl attrs ~contents:(exp_term e v) out tab;
+ exp_term e t out tab
+ | B.Bind (a, b, t) ->
+ let a = rename C.start e a in
+ exp_bind e a b out tab;
+ exp_term (B.push e B.empty a b) t out tab
+
+and exp_bind e a b out tab = match b with
+ | B.Abst w ->
+ let attrs = [X.name a; X.mark a] in
+ X.tag X.abst attrs ~contents:(exp_term e w) out tab
+ | B.Abbr v ->
+ let attrs = [X.name a; X.mark a] in
+ X.tag X.abbr attrs ~contents:(exp_term e v) out tab
+ | B.Void ->
+ let attrs = [X.name a; X.mark a] in
+ X.tag X.void attrs out tab
+
+let export_term = exp_term B.empty