- 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