In place of conclude, obtain FIXMEXXX is now generated when required.

[helm.git] / helm / software / components / content_pres / boxPp.ml

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index 2957a3975446f48c3c0c69e763d3ba45eccd43cc..5719f2b69203912cb5a1983c48d16f849f43f075 100644 (file)
--- a/helm/software/components/content_pres/boxPp.ml
+++ b/helm/software/components/content_pres/boxPp.ml
@@ -31,7 +31,7 @@ module Pres = Mpresentation
 
 let string_space = " "
 let string_space_len = String.length string_space
-let string_indent = string_space
+let string_indent = (* string_space *) ""
 let string_indent_len = String.length string_indent
 let string_ink = "##"
 let string_ink_len = String.length string_ink
@@ -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,11 +193,15 @@ let render_to_strings choose_action size markup =
     | Pres.Mgliph (_, s) -> fixed_rendering s
     | Pres.Mo (_, s) ->
         let s =
-          if String.length s > 1 then
-            (* heuristic to guess which operators need to be expanded in their
-             * TeX like format *)
-            Utf8Macro.tex_of_unicode s ^ " "
-          else 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
     | Pres.Mspace _ -> fixed_rendering string_space
@@ -236,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)