From: Stefano Zacchiroli Date: Tue, 6 Sep 2005 16:50:33 +0000 (+0000) Subject: bugfix: avoid losing attributes on boxes which have a single children X-Git-Tag: V_0_1_2_1~67 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e8363bec852afb37160d8144db8d94bbff447d6;p=helm.git bugfix: avoid losing attributes on boxes which have a single children this used to cause impossibility of selecting a let .. in term --- diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 8d548e1eb..60ee0dfb3 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -35,13 +35,6 @@ let atop_attributes = [None, "linethickness", "0pt"] let to_unicode = Utf8Macro.unicode_of_tex -(* let rec make_attributes l1 = function - | [] -> [] - | None :: tl -> make_attributes (List.tl l1) tl - | Some s :: tl -> - let p,n = List.hd l1 in - prerr_endline (Printf.sprintf "make_attributes %s %s" n s); - (p,n,s) :: make_attributes (List.tl l1) tl *) let rec make_attributes l1 = function | [] -> [] | hd :: tl -> @@ -49,18 +42,21 @@ let rec make_attributes l1 = function | None -> make_attributes (List.tl l1) tl | Some s -> let p,n = List.hd l1 in -(* prerr_endline (Printf.sprintf "make_attributes %s %s" n s); *) hd := None; (p,n,s) :: make_attributes (List.tl l1) tl) let box_of_mpres = function - Mpresentation.Mobject (_, box) -> box + | Mpresentation.Mobject (attrs, box) -> + assert (attrs = []); + box | mpres -> Box.Object ([], mpres) let mpres_of_box = function - Box.Object (_, mpres) -> mpres + | Box.Object (attrs, mpres) -> + assert (attrs = []); + mpres | box -> Mpresentation.Mobject ([], box) let rec genuine_math = @@ -86,9 +82,19 @@ let rec promote_to_math = let small_skip = Mpresentation.Mspace (RenderingAttrs.small_skip_attributes `MathML) +let rec add_mpres_attributes new_attr = function + | Mpresentation.Mobject (attr, box) -> + Mpresentation.Mobject (attr, add_box_attributes new_attr box) + | mpres -> + Mpresentation.set_attr (new_attr @ Mpresentation.get_attr mpres) mpres +and add_box_attributes new_attr = function + | Box.Object (attr, mpres) -> + Box.Object (attr, add_mpres_attributes new_attr mpres) + | box -> Box.set_attr (new_attr @ Box.get_attr box) box + let box_of mathonly spec attrs children = match children with - | [t] -> t + | [t] -> add_mpres_attributes attrs t | _ -> let kind, spacing, indent = spec in let dress children =