- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / xml / xmlLibrary.ml

diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
index a9b1e5a1cd195662867d1f33a375882b98d5d226..af6245c9f4371d3211f2429f43f516c184969d7e 100644 (file)
--- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml
+++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml
@@ -14,6 +14,7 @@ module U = NUri
 module C = Cps
 module H = Hierarchy
 module E = Entity
+module N = Level
 
 (* internal functions *******************************************************)
 
@@ -106,6 +107,9 @@ let mark a =
    let f i = "mark", string_of_int i in
    E.mark err f a
 
+let level n =
+   "level", N.to_string n
+
 (* TODO: the string s must be quoted *)
 let meta a =
    let err () = "meta", "" in
@@ -121,9 +125,9 @@ let export_entity pp_term si xdir (a, u, b) =
    let a = E.Name (U.name_of_uri u, true) :: a in
    let attrs = [uri u; name a; mark a; meta a] in 
    let contents = match b with
-      | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w) 
-      | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
-      | E.Void   -> assert false
+      | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w) 
+      | E.Abbr v      -> tag "ABBR" attrs ~contents:(pp_term v)
+      | E.Void        -> assert false
    in
    let opts = if si then "si" else "" in
    let shp = H.string_of_graph () in