X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fxml%2Fxml.ml;h=9dcd16fc0780e897518c71c49ea1b3d2ee6a8d34;hb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;hp=6670e1f1923220f0713cec65157730b83338d0c2;hpb=b266dce15b2f669a70daaee3bd0887f8d9c345b2;p=helm.git

diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml
index 6670e1f19..9dcd16fc0 100644
--- a/helm/ocaml/xml/xml.ml
+++ b/helm/ocaml/xml/xml.ml
@@ -38,44 +38,55 @@
 
 
 (* the type token for XML cdata, empty elements and not-empty elements *)
-(* Usage:                                                                *)
-(*  Str cdata                                                            *)
-(*  Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen]   *)
-(*  NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
-(*          content                                                      *)
-type token = Str of string
-           | Empty of string * (string * string) list
-	   | NEmpty of string * (string * string) list * token Stream.t
+(* Usage:                                                             *)
+(*  Str cdata                                                         *)
+(*  Empty (prefix, element_name,                                      *)
+(*   [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen]  *)
+(*  NEmpty (prefix, element_name,                                     *)
+(*   [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen], *)
+(*    content                                                         *)
+type token =
+   Str of string
+ | Empty of string option * string * (string option * string * string) list
+ | NEmpty of string option * string * (string option * string * string) list *
+    token Stream.t
 ;;
 
 (* currified versions of the constructors make the code more readable *)
-let xml_empty name attrs = [< 'Empty(name,attrs) >]
-let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
-let xml_cdata str = [< 'Str str >]
+let xml_empty ?prefix name attrs =
+ [< 'Empty(prefix,name,attrs) >]
+let xml_nempty ?prefix name attrs content =
+ [< 'NEmpty(prefix,name,attrs,content) >]
+let xml_cdata str =
+ [< 'Str str >]
 
 (** low level for other PPs: pretty print each token of strm applying 'f' to a
 canonical string representation of each token *)
 let pp_gen f strm =
+ let pprefix =
+  function
+     None -> ""
+   | Some p -> p ^ ":" in
  let rec pp_r m =
   parser
   | [< 'Str a ; s >] ->
       print_spaces m ;
       f (a ^ "\n") ;
       pp_r m s
-  | [< 'Empty(n,l) ; s >] ->
+  | [< 'Empty(p,n,l) ; s >] ->
       print_spaces m ;
-      f ("<" ^ n) ;
-      List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
+      f ("<" ^ (pprefix p) ^ n) ;
+      List.iter (fun (p,n,v) -> f (" " ^ (pprefix p) ^ n ^ "=\"" ^ v ^ "\"")) l;
       f "/>\n" ;
       pp_r m s
-  | [< 'NEmpty(n,l,c) ; s >] ->
+  | [< 'NEmpty(p,n,l,c) ; s >] ->
       print_spaces m ;
-      f ("<" ^ n) ;
-      List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
+      f ("<" ^ (pprefix p) ^ n) ;
+      List.iter (fun (p,n,v) -> f (" " ^ (pprefix p) ^ n ^ "=\"" ^ v ^ "\"")) l;
       f ">\n" ;
       pp_r (m+1) c ;
       print_spaces m ;
-      f ("</" ^ n ^ ">\n") ;
+      f ("</" ^ (pprefix p) ^ n ^ ">\n") ;
       pp_r m s
   | [< >] -> ()
  and print_spaces m =