X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fbox.ml;h=96c55b18ae4c01c7ec991e85ec47bdb035833d3c;hb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;hp=386fabd0bfb65a9b4e721b8e33fe1215bfd7af15;hpb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/box.ml b/helm/ocaml/cic_transformations/box.ml
index 386fabd0b..96c55b18a 100644
--- a/helm/ocaml/cic_transformations/box.ml
+++ b/helm/ocaml/cic_transformations/box.ml
@@ -39,6 +39,8 @@ type
   | Ink of attr
   | H of attr * ('expr box) list
   | V of attr * ('expr box) list
+  | HV of attr * ('expr box) list
+  | HOV of attr * ('expr box) list
   | Object of attr * 'expr
   | Action of attr * ('expr box) list
 
@@ -51,6 +53,13 @@ let indent t = H([],[skip;t]);;
 
 (* BoxML prefix *)
 let prefix = "b";;
+
+let tag_of_box = function
+  | H _ -> "h"
+  | V _ -> "v"
+  | HV _ -> "hv"
+  | HOV _ -> "hov"
+  | _ -> assert false
  
 let box2xml ~obj2xml box =
   let rec aux =
@@ -59,12 +68,11 @@ let box2xml ~obj2xml box =
         Text (attr,s) -> X.xml_nempty ~prefix "text" attr (X.xml_cdata s)
       | Space attr -> X.xml_empty ~prefix "space" attr
       | Ink attr -> X.xml_empty ~prefix "ink" attr
-      | H (attr,l) ->
-          X.xml_nempty ~prefix "h" attr 
-            [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
-            >]
-      | V (attr,l) ->
-          X.xml_nempty ~prefix "v" attr 
+      | H (attr,l)
+      | V (attr,l)
+      | HV (attr,l)
+      | HOV (attr,l) as box ->
+          X.xml_nempty ~prefix (tag_of_box box) attr 
             [< (List.fold_right (fun x i -> [< (aux x) ; i >]) l [<>])
             >]
       | Object (attr,m) ->
@@ -82,6 +90,8 @@ let rec map f = function
   | (Ink _) as box -> box
   | H (attr, l) -> H (attr, List.map (map f) l)
   | V (attr, l) -> V (attr, List.map (map f) l)
+  | HV (attr, l) -> HV (attr, List.map (map f) l)
+  | HOV (attr, l) -> HOV (attr, List.map (map f) l)
   | Action (attr, l) -> Action (attr, List.map (map f) l)
   | Object (attr, obj) -> Object (attr, f obj)
 ;;