X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FboxPp.ml;h=0d58d97643a17aa147d117d006ed4cc8cec212d5;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=5719f2b69203912cb5a1983c48d16f849f43f075;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index 5719f2b69..0d58d9764 100644
--- a/helm/software/components/content_pres/boxPp.ml
+++ b/helm/software/components/content_pres/boxPp.ml
@@ -93,7 +93,7 @@ let fixed_rendering s =
   let s_len = String.length s in
   (fun _ -> s_len, [s])
 
-let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup =
+let render_to_strings ~map_unicode_to_tex choose_action size markup =
   let max_size = max_int in
   let rec aux_box =
     function
@@ -185,6 +185,7 @@ let render_to_strings ?(map_unicode_to_tex = true) 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)
@@ -198,8 +199,8 @@ let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup =
               s
             else
               match Utf8Macro.tex_of_unicode s with
-              | Some s -> s ^ " "
-              | None -> " " ^ s ^ " "
+              | s::_ -> s ^ " "
+              | [] -> " " ^ s ^ " "
           end else
             s
         in
@@ -209,11 +210,11 @@ let render_to_strings ?(map_unicode_to_tex = true) 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 = true) 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 _ ->
@@ -240,7 +241,7 @@ let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup =
   in
   snd (aux_mpres markup size)
 
-let render_to_string ?map_unicode_to_tex choose_action size markup =
+let render_to_string ~map_unicode_to_tex choose_action size markup =
   String.concat "\n"
-    (render_to_strings ?map_unicode_to_tex choose_action size markup)
+    (render_to_strings ~map_unicode_to_tex choose_action size markup)