1. bug fixed: Unicode characters that are not mapped to TeX macros used to

[helm.git] / helm / software / components / grafite_parser / print_grammar.ml

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index 6a05865de8f2c9149b6e6a6c6e7ca4b274afd315..f05b77a11b029fa75d60ea5d920793ebca2767fa 100644 (file)
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/components/grafite_parser/print_grammar.ml
@@ -28,11 +28,15 @@
 open Gramext 
 
 let tex_of_unicode s =
+(*CSC: ??????? What's the meaning of this function?
   let contractions = ("\\Longrightarrow","=>") :: [] in
   if String.length s <= 1 then s
   else  (* probably an extended unicode symbol *)
     let s = Utf8Macro.tex_of_unicode s in
     try List.assoc s contractions with Not_found -> s
+*) match Utf8Macro.tex_of_unicode s with
+      Some s -> s
+    | None -> s
 
 let needs_brackets t =
   let rec count_brothers = function