]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/box.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_notation / box.ml
index 3c079d3162701d72397abad40d84a8d8fd09843d..c11558a2796040a01b633a892f481d646bd310b8 100644 (file)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -111,11 +111,40 @@ let document_of_box ~obj2xml pres =
 
 let b_h a b = H(a,b)
 let b_v a b = V(a,b)
-let b_hv a b = H(a,b)
-let b_hov a b = V(a,b)
+let b_hv a b = HV(a,b)
+let b_hov a b = HOV(a,b)
 let b_text a b = Text(a,b)
 let b_object b = Object ([],b)
 let b_indent = indent
 let b_space = Space [None, "width", "0.5em"]
 let b_kw = b_text (RenderingAttrs.object_keyword_attributes `BoxML)
 
+let pp_attr attr =
+  let pp (ns, n, v) =
+    Printf.sprintf "%s%s=%s" (match ns with None -> "" | Some s -> s ^ ":") n v
+  in
+  String.concat " " (List.map pp attr)
+
+let get_attr = function
+  | Text (attr, _)
+  | Space attr
+  | Ink attr
+  | H (attr, _)
+  | V (attr, _)
+  | HV (attr, _)
+  | HOV (attr, _)
+  | Object (attr, _)
+  | Action (attr, _) ->
+      attr
+
+let set_attr attr = function
+  | Text (_, x) -> Text (attr, x)
+  | Space _ -> Space attr
+  | Ink _ -> Ink attr
+  | H (_, x) -> H (attr, x)
+  | V (_, x) -> V (attr, x)
+  | HV (_, x) -> HV (attr, x)
+  | HOV (_, x) -> HOV (attr, x)
+  | Object (_, x) -> Object (attr, x)
+  | Action (_, x) -> Action (attr, x)
+