From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Nov 2005 15:08:19 +0000 (+0000)
Subject: ligature expansion now considers also tex macros
X-Git-Tag: V_0_7_2_3~130
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d9f8695ea82b736d8806cd63e85cc3d7d88048e;p=helm.git

ligature expansion now considers also tex macros
---

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 17d77f902..5d2dae341 100644
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -255,14 +255,12 @@ let rec comment_token acc depth =
       let acc = acc ^ Ulexing.utf8_lexeme lexbuf in
       comment_token acc depth lexbuf
 
-let lookup_ligatures lexeme = List.rev (Hashtbl.find_all ligatures lexeme)
-
   (** @param k continuation to be invoked when no ligature has been found *)
 let rec ligatures_token k =
   lexer
   | ligature ->
       let lexeme = Ulexing.utf8_lexeme lexbuf in
-      (match lookup_ligatures lexeme with
+      (match List.rev (Hashtbl.find_all ligatures lexeme) with
       | [] -> (* ligature not found, rollback and try default lexer *)
           Ulexing.rollback lexbuf;
           k lexbuf
@@ -341,3 +339,10 @@ let level1_pattern_lexer = mk_lexer level1_pattern_token
 let level2_ast_lexer = mk_lexer level2_ast_token
 let level2_meta_lexer = mk_lexer level2_meta_token
 
+let lookup_ligatures lexeme =
+  try
+    if lexeme.[0] = '\\'
+    then [ Utf8Macro.expand (String.sub lexeme 1 (String.length lexeme - 1)) ]
+    else List.rev (Hashtbl.find_all ligatures lexeme)
+  with Invalid_argument _ | Utf8Macro.Macro_not_found _ as exn -> []
+