From 4d9f8695ea82b736d8806cd63e85cc3d7d88048e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 4 Nov 2005 15:08:19 +0000 Subject: [PATCH] ligature expansion now considers also tex macros --- helm/ocaml/cic_notation/cicNotationLexer.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) 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 -> [] + -- 2.39.2