X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FboxPp.ml;h=0d58d97643a17aa147d117d006ed4cc8cec212d5;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=a51920c799416b2db97b3e7e22ee4196ffbefd1a;hpb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;p=helm.git diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml index a51920c79..0d58d9764 100644 --- a/helm/software/components/content_pres/boxPp.ml +++ b/helm/software/components/content_pres/boxPp.ml @@ -185,6 +185,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = and aux_mpres = let text s = Pres.Mtext ([], s) in let mrow c = Pres.Mrow ([], c) in + let parentesize s = s in function | Pres.Mi (_, s) | Pres.Mn (_, s) @@ -209,11 +210,11 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let children' = List.map aux_mpres children in (fun size -> render_row size false children') | Pres.Mfrac (_, m, n) -> - aux_mpres (mrow [ text "\\frac("; text ")"; text "("; n; text ")" ]) - | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text "\\sqrt("; m; text ")" ]) + aux_mpres (mrow [ text " \\frac "; parentesize m ; text " "; parentesize n; text " " ]) + | Pres.Msqrt (_, m) -> aux_mpres (mrow [ text " \\sqrt "; parentesize m; text " "]) | Pres.Mroot (_, r, i) -> aux_mpres (mrow [ - text "\\root("; i; text ")"; text "\\of("; r; text ")" ]) + text " \\root "; parentesize i; text " \\of "; parentesize r; text " " ]) | Pres.Mstyle (_, m) | Pres.Merror (_, m) | Pres.Mpadded (_, m) @@ -222,13 +223,13 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = | Pres.Mfenced (_, children) -> aux_mpres (mrow children) | Pres.Maction (_, []) -> assert false | Pres.Msub (_, m, n) -> - aux_mpres (mrow [ text "("; m; text ")\\sub("; n; text ")" ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\sub "; parentesize n; text " " ]) | Pres.Msup (_, m, n) -> - aux_mpres (mrow [ text "("; m; text ")\\sup("; n; text ")" ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\sup "; parentesize n; text " " ]) | Pres.Munder (_, m, n) -> - aux_mpres (mrow [ text "("; m; text ")\\below("; n; text ")" ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\below "; parentesize n; text " " ]) | Pres.Mover (_, m, n) -> - aux_mpres (mrow [ text "("; m; text ")\\above("; n; text ")" ]) + aux_mpres (mrow [ text " "; parentesize m; text " \\above "; parentesize n; text " " ]) | Pres.Msubsup _ | Pres.Munderover _ | Pres.Mtable _ ->