X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationPres.ml;h=395cab6c29927e01cc1760ec1ac6ccc28e6fd87f;hb=e5014674aed0dab6f3aa43773c8caeffcfe0ac32;hp=a14ff349d8c5db23e9d9cebd83071e341f15f8c9;hpb=915c3e1993cad4dcadefe7e6886e6cb8feefae8b;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index a14ff349d..395cab6c2 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -33,10 +33,6 @@ let binder_attributes = [None, "mathcolor", "blue"] let indent_attributes = [None, "indent", "1em"] let keyword_attributes = [None, "mathcolor", "blue"] -let mpres_arrow = Mpresentation.Mo (binder_attributes, "->") - (* TODO unicode symbol "to" *) -let mpres_implicit = Mpresentation.Mtext ([], "?") - let to_unicode s = try if s.[0] = '\\' then @@ -68,32 +64,33 @@ let genuine_math = let box_of mathonly spec attrs children = match children with - | [t] -> t - | _ -> - let kind, spacing, indent = spec in - let rec dress = function - | [] -> [] - | [hd] -> [hd] - | hd :: tl -> hd :: Mpresentation.Mtext ([], " ") :: dress tl - in - if mathonly then Mpresentation.Mrow (attrs, dress children) - else - let attrs' = - if spacing then [None, "spacing", "0.5em"] else [] - @ if indent then [None, "indent", "0em 0.5em"] else [] - @ attrs - in - match kind with - | CicNotationPt.H when List.for_all genuine_math children -> - Mpresentation.Mrow (attrs', children) - | CicNotationPt.H -> - mpres_of_box (Box.H (attrs', List.map box_of_mpres children)) - | CicNotationPt.V -> - mpres_of_box (Box.V (attrs', List.map box_of_mpres children)) - | CicNotationPt.HV -> - mpres_of_box (Box.HV (attrs', List.map box_of_mpres children)) - | CicNotationPt.HOV -> - mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children)) + | [t] -> t + | _ -> + let kind, spacing, indent = spec in + let dress children = + if spacing then + CicNotationUtil.dress (Mpresentation.Mtext ([], " ")) children + else + children + in + if mathonly then Mpresentation.Mrow (attrs, dress children) + else + let attrs' = + (if spacing then [None, "spacing", "0.5em"] else []) + @ (if indent then [None, "indent", "0em 0.5em"] else []) + @ attrs + in + match kind with + | CicNotationPt.H when List.for_all genuine_math children -> + Mpresentation.Mrow (attrs', dress children) + | CicNotationPt.H -> + mpres_of_box (Box.H (attrs', List.map box_of_mpres children)) + | CicNotationPt.V -> + mpres_of_box (Box.V (attrs', List.map box_of_mpres children)) + | CicNotationPt.HV -> + mpres_of_box (Box.HV (attrs', List.map box_of_mpres children)) + | CicNotationPt.HOV -> + mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children)) let open_paren = Mpresentation.Mo ([], "(") let closed_paren = Mpresentation.Mo ([], ")") @@ -211,7 +208,8 @@ let render ids_to_uris = assert false and aux_attribute xmlattrs mathonly xref pos prec uris t = function - | `Loc _ -> aux xmlattrs mathonly xref pos prec uris t + | `Loc _ + | `Raw _ -> aux xmlattrs mathonly xref pos prec uris t | `Level (child_prec, child_assoc) -> let t' = aux xmlattrs mathonly xref pos child_prec uris t in add_parens child_prec child_assoc pos prec t' @@ -238,39 +236,53 @@ let render ids_to_uris = P.Mfrac (atop_attributes @ attrs, invoke' t1, invoke' t2) | A.Sqrt t -> P.Msqrt (attrs, invoke' t) | A.Root (t1, t2) -> P.Mroot (attrs, invoke' t1, invoke' t2) - | A.Box (kind, terms) -> - let children = aux_children mathonly xref pos prec uris terms in + | A.Box ((_, spacing, _) as kind, terms) -> + let children = aux_children mathonly spacing xref pos prec uris (CicNotationUtil.ungroup terms) in box_of mathonly kind attrs children + | A.Group terms -> + let children = aux_children false mathonly xref pos prec uris (CicNotationUtil.ungroup terms) in + box_of mathonly (A.H, false, false) attrs children | A.Break -> assert false (* TODO? *) - and aux_children mathonly xref pos prec uris terms = - let rec aux_list first = + and aux_children mathonly spacing xref pos prec uris terms = + let find_clusters = + let rec aux_list first clusters acc = + function + [] when acc = [] -> List.rev clusters + | [] -> aux_list first (List.rev acc :: clusters) [] [] + | (A.Layout A.Break) :: tl when acc = [] -> aux_list first clusters [] tl + | (A.Layout A.Break) :: tl -> aux_list first (List.rev acc :: clusters) [] tl + | [hd] -> + let pos' = + if first then + pos + else + match pos with + `None -> `Right + | `Inner -> `Inner + | `Right -> `Right + | `Left -> `Inner + in + aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) [] + | hd :: tl -> + let pos' = + match pos, first with + `None, true -> `Left + | `None, false -> `Inner + | `Left, true -> `Left + | `Left, false -> `Inner + | `Right, _ -> `Inner + | `Inner, _ -> `Inner + in + aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) tl + in + aux_list true [] [] + in + let boxify_pres = function - [] -> [] - | [t] -> - assert (not first); - let pos' = - match pos with - `None -> `Right - | `Inner -> `Inner - | `Right -> `Right - | `Left -> `Inner - in - [aux [] mathonly xref pos' prec uris t] - | t :: tl -> - let pos' = - match pos, first with - `None, true -> `Left - | `None, false -> `Inner - | `Left, true -> `Left - | `Left, false -> `Inner - | `Right, _ -> `Inner - | `Inner, _ -> `Inner - in - (aux [] mathonly xref pos' prec uris t) :: aux_list false tl + [t] -> t + | tl -> box_of mathonly (A.H, spacing, false) [] tl in - match terms with - | [t] -> [aux [] mathonly xref pos prec uris t] - | tl -> aux_list true tl + List.map boxify_pres (find_clusters terms) in aux [] false None `None 0 []