From: Stefano Zacchiroli <zack@upsilon.cc>
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 @@
 
 <entities-table>
   <entity name="def" value="&#x0225d;"/>  <!-- ≝ -->
+  <entity name="neq" value="&#x02260;"/>  <!-- ≠ -->
 </entities-table>
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"