From: Stefano Zacchiroli Date: Mon, 25 Jul 2005 10:13:30 +0000 (+0000) Subject: - addded unicode_of_tex X-Git-Tag: V_0_7_2~94 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7b7e9b07ee3bb4d12d522b2deae3aa5b62df4793;p=helm.git - addded unicode_of_tex - added \neq macro --- diff --git a/helm/ocaml/utf8_macros/data/extra-entities.xml b/helm/ocaml/utf8_macros/data/extra-entities.xml index 991c2d84b..e99c548e2 100644 --- a/helm/ocaml/utf8_macros/data/extra-entities.xml +++ b/helm/ocaml/utf8_macros/data/extra-entities.xml @@ -2,4 +2,5 @@ + diff --git a/helm/ocaml/utf8_macros/utf8Macro.ml b/helm/ocaml/utf8_macros/utf8Macro.ml index 4e0bc9498..51465046b 100644 --- a/helm/ocaml/utf8_macros/utf8Macro.ml +++ b/helm/ocaml/utf8_macros/utf8Macro.ml @@ -31,3 +31,10 @@ let expand macro = Hashtbl.find Utf8MacroTable.macro2utf8 macro with Not_found -> raise (Macro_not_found macro) +let unicode_of_tex s = + try + if s.[0] = '\\' then + expand (String.sub s 1 (String.length s - 1)) + else s + with Macro_not_found _ -> s + diff --git a/helm/ocaml/utf8_macros/utf8Macro.mli b/helm/ocaml/utf8_macros/utf8Macro.mli index bf3fc16b4..9220365d1 100644 --- a/helm/ocaml/utf8_macros/utf8Macro.mli +++ b/helm/ocaml/utf8_macros/utf8Macro.mli @@ -26,7 +26,12 @@ exception Macro_not_found of string exception Utf8_not_found of string - (* @param macro name + (** @param macro name @return utf8 string *) val expand: string -> string + (** @param tex TeX like command (e.g. \forall, \lnot, ...) + * @return unicode character corresponding to the command if it exists, or the + * unchanged command if not *) +val unicode_of_tex: string -> string + diff --git a/helm/ocaml/utf8_macros/utf8MacroTable.ml b/helm/ocaml/utf8_macros/utf8MacroTable.ml index d33361f3d..a97e8faf1 100644 --- a/helm/ocaml/utf8_macros/utf8MacroTable.ml +++ b/helm/ocaml/utf8_macros/utf8MacroTable.ml @@ -2012,6 +2012,7 @@ let _ = Hashtbl.add macro2utf8 "rarrpl" "\226\165\133" let _ = Hashtbl.add macro2utf8 "auml" "\195\164" let _ = Hashtbl.add macro2utf8 "bmod" "mod" let _ = Hashtbl.add macro2utf8 "SquareSuperset" "\226\138\144" +let _ = Hashtbl.add macro2utf8 "neq" "\226\137\160" let _ = Hashtbl.add macro2utf8 "circleddash" "\226\138\157" let _ = Hashtbl.add macro2utf8 "xrarr" "\239\149\183" let _ = Hashtbl.add macro2utf8 "barwed" "\226\138\188"