]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgOutput.ml
- kernel parameters indication added to exported objects (xml)
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml
index 1aa3f9db7d4ecc0ddda91c04138d7bb9db7c140c..fb33da537a7b59bc2eb4a6cf113e1641702e1dda 100644 (file)
@@ -15,7 +15,6 @@ module U = NUri
 module L = Log
 module H = Hierarchy
 module O = Output
-module CL = CommonLibrary
 module B = Brg
 
 (* nodes count **************************************************************)
@@ -32,7 +31,7 @@ type counters = {
    tabsts: int;
    tabbrs: int;
    tvoids: int;
-   uris  : U.uri list;
+   uris  : B.uri list;
    nodes : int;
    xnodes: int
 }
@@ -222,16 +221,16 @@ and exp_bind a frm = function
    | B.Void   ->
       F.fprintf frm "<Void%a/>" id a
 
-let export_obj frm = function
+let exp_obj frm = function
    | _, uri, B.Abst w -> 
       let str = U.string_of_uri uri in
-      F.fprintf frm "%s@,@,<ABST uri=%S>%a</ABST>" 
-         (CL.doctype "ABST") str exp_boxed w
+      F.fprintf frm "<ABST uri=%S/>@,%a" str exp_term w
    | _, uri, B.Abbr v -> 
       let str = U.string_of_uri uri in
-      F.fprintf frm "%s@,@,<ABBR uri=%S>%a</ABBR>"
-         (CL.doctype "ABBR") str exp_boxed v
+      F.fprintf frm "<ABBR uri=%S/>@,%a" str exp_term v
    | _, uri, B.Void   -> 
       let str = U.string_of_uri uri in
-      F.fprintf frm "%s@,@,<VOID uri=%S/>" 
-         (CL.doctype "VOID") str
+      F.fprintf frm "<VOID uri=%S/>" str
+
+let export_obj frm obj =
+   F.fprintf frm "@,@[<v3>   %a@]@," exp_obj obj