From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 6 Sep 2005 16:48:04 +0000 (+0000)
Subject: added {get,set,pp}_attr
X-Git-Tag: V_0_1_2_1~70
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=81c28c560eeb8eab9f185ffc1717190d0fe571e8;p=helm.git

added {get,set,pp}_attr
---

diff --git a/helm/ocaml/cic_notation/box.ml b/helm/ocaml/cic_notation/box.ml
index 7c4026d81..c11558a27 100644
--- a/helm/ocaml/cic_notation/box.ml
+++ b/helm/ocaml/cic_notation/box.ml
@@ -119,3 +119,32 @@ 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)
+
diff --git a/helm/ocaml/cic_notation/box.mli b/helm/ocaml/cic_notation/box.mli
index 296695780..56c086964 100644
--- a/helm/ocaml/cic_notation/box.mli
+++ b/helm/ocaml/cic_notation/box.mli
@@ -46,6 +46,9 @@ type
 
 and attr = (string option * string * string) list
 
+val get_attr: 'a box -> attr
+val set_attr: attr -> 'a box -> 'a box
+
 val smallskip : 'expr box
 val skip: 'expr box
 val indent : 'expr box -> 'expr box
@@ -71,3 +74,5 @@ val b_indent: 'expr box -> 'expr box
 val b_space: 'expr box
 val b_kw: string -> 'expr box
 
+val pp_attr: attr -> string
+