X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fbox.ml;h=c11558a2796040a01b633a892f481d646bd310b8;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=241214f9ce883aa993deef1695458b2c1df3d3dc;hpb=82fa16ab2ddac93fdfb976c952ad31315c15d8b9;p=helm.git diff --git a/helm/ocaml/cic_notation/box.ml b/helm/ocaml/cic_notation/box.ml index 241214f9c..c11558a27 100644 --- a/helm/ocaml/cic_notation/box.ml +++ b/helm/ocaml/cic_notation/box.ml @@ -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 @@ -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) +