X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2FboxPp.ml;h=ca51c0ed3e46d8c14730301bd7640bfb598d6a7e;hb=78f2fb8fcf0bbd2521b67e4366b734ad88ebdc68;hp=b9bb9fbbd5badc06ef55a36ca418471731559db2;hpb=f9512e878bd27f8cb5261bb18b0da0d42c8184d0;p=helm.git

diff --git a/components/content_pres/boxPp.ml b/components/content_pres/boxPp.ml
index b9bb9fbbd..ca51c0ed3 100644
--- a/components/content_pres/boxPp.ml
+++ b/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 choose_action size markup =
+let render_to_strings ?(map_unicode_to_tex = true) choose_action size markup =
   let max_size = max_int in
   let rec aux_box =
     function
@@ -193,14 +193,17 @@ let render_to_strings choose_action size markup =
     | Pres.Mgliph (_, s) -> fixed_rendering s
     | Pres.Mo (_, s) ->
         let s =
-         if String.length s = 1 && Char.code s.[0] < 128 then
-          s
-         else
-          match Utf8Macro.tex_of_unicode s with
-             Some s -> s ^ " "
-           | None -> s
+          if map_unicode_to_tex then begin
+            if String.length s = 1 && Char.code s.[0] < 128 then
+              s
+            else
+              match Utf8Macro.tex_of_unicode s with
+              | Some s -> s ^ " "
+              | None -> s
+          end else
+            s
         in
-         fixed_rendering s
+        fixed_rendering s
     | Pres.Mspace _ -> fixed_rendering string_space
     | Pres.Mrow (attrs, children) ->
         let children' = List.map aux_mpres children in
@@ -237,6 +240,7 @@ let render_to_strings choose_action size markup =
   in
   snd (aux_mpres markup size)
 
-let render_to_string choose_action size markup =
-  String.concat "\n" (render_to_strings 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)