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
| 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 String.length s = 1 && Char.code s.[0] < 128 then
+ s
+ else
+ match Utf8Macro.tex_of_unicode s with
+ Some s -> s ^ " "
+ | None -> 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