]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlLibrary.ml
- the disambiguation of unified binders continues
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
index 1e2bd4de4d5e015ff100fcc6f09e3c5794a89059..2e3fdef8a6d9322725977a6c45cee3bf121fd974 100644 (file)
@@ -16,7 +16,6 @@ module H = Hierarchy
 module G = Options
 module E = Entity
 module N = Level
-module Q = Ccs
 
 (* internal functions *******************************************************)
 
@@ -105,8 +104,8 @@ let apix a =
    let f i = "age", string_of_int i in
    E.apix err f a
 
-let level n =
-   "level", N.to_string n
+let level st n =
+   "level", N.to_string st n
 
 let meta a =
    let map = function
@@ -117,9 +116,6 @@ let meta a =
    in
    "meta", String.concat " " (List.rev_map map a.E.r_meta)
 
-let arity l =
-   "arity", string_of_int (List.length l)
-
 (* TODO: the string tx must be quoted *)
 let info a =
    let err () = ["lang", ""; "info", ""] in
@@ -144,36 +140,3 @@ let export_entity pp_term (ra, na, u, b) =
    let attrs = [xmlns; "hierarchy", shp; "options", opts] in
    tag obj_root attrs ~contents out 0;
    close_out och
-
-let prec_map (i, _) = string_of_int i
-
-let next_map (_, i) = string_of_int i
-
-let marks = function
-   | [] -> "mark", ""
-   | l  -> "mark", String.concat " " (List.rev_map string_of_int l)
-
-let precs = function
-   | [] -> "prec", ""
-   | l  -> "prec", String.concat " " (List.rev_map prec_map l)
-
-let nexts = function
-   | [] -> "next", ""
-   | l  -> "next", String.concat " " (List.rev_map next_map l)
-(*
-let export_csys s = 
-   let path = path_of_uri !G.xdir s.Q.buri in
-   let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
-   let name = F.concat path (ccs_name ^ ext) in
-   let och = open_out name in
-   let out = output_string och in
-   xml out "1.0" "UTF-8"; doctype out ccs_root system;
-   let attrs = [xmlns; uri s.Q.buri] in
-   let contents out tab =
-      tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
-      tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
-      tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
-   in
-   tag ccs_root attrs ~contents out 0;
-   close_out och
-*)