From 81c28c560eeb8eab9f185ffc1717190d0fe571e8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 6 Sep 2005 16:48:04 +0000 Subject: [PATCH] added {get,set,pp}_attr --- helm/ocaml/cic_notation/box.ml | 29 +++++++++++++++++++++++++++++ helm/ocaml/cic_notation/box.mli | 5 +++++ 2 files changed, 34 insertions(+) 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 + -- 2.39.2