| Box.Space _ -> fixed_rendering string_space
| Box.Ink _ -> fixed_rendering string_ink
| Box.Action (_, []) -> assert false
| Box.Space _ -> fixed_rendering string_space
| Box.Ink _ -> fixed_rendering string_ink
| Box.Action (_, []) -> assert false
| Box.Object (_, o) -> aux_mpres o
| Box.H (attrs, children) ->
let spacing = want_spacing attrs in
| Box.Object (_, o) -> aux_mpres o
| Box.H (attrs, children) ->
let spacing = want_spacing attrs in
- 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 String.length s = 1 && Char.code s.[0] < 128 then
+ s
+ else
+ match Utf8Macro.tex_of_unicode s with
+ Some s -> s ^ " "
+ | None -> s
| Pres.Mspace _ -> fixed_rendering string_space
| Pres.Mrow (attrs, children) ->
let children' = List.map aux_mpres children in
| Pres.Mspace _ -> fixed_rendering string_space
| Pres.Mrow (attrs, children) ->
let children' = List.map aux_mpres children in
-let render_to_string size markup =
- String.concat "\n" (render_to_strings size markup)
+let render_to_string choose_action size markup =
+ String.concat "\n" (render_to_strings choose_action size markup)