From 921ba3b356400323b440a073a7030c5386d3b421 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 4 Nov 2005 14:03:47 +0000 Subject: [PATCH] added ligatures expansion support functions --- helm/ocaml/cic_notation/cicNotationLexer.ml | 17 ++++++++++++++--- helm/ocaml/cic_notation/cicNotationLexer.mli | 5 ++++- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 9fa6270ee..17d77f902 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -34,9 +34,19 @@ let regexp number = xml_digit+ let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ] + (* must be in sync with "is_ligature_char" below *) let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ] let regexp ligature = ligature_char ligature_char+ +let is_ligature_char = + (* must be in sync with "regexp ligature_char" above *) + let chars = "'`~!?@*()[]<>-+=|:;.,/\"" in + (fun char -> + (try + ignore (String.index chars char); + true + with Not_found -> false)) + let regexp ident_decoration = '\'' | '?' | '`' let regexp ident_cont = ident_letter | xml_digit | '_' let regexp ident = ident_letter ident_cont* ident_decoration* @@ -245,17 +255,18 @@ 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 Hashtbl.find_all ligatures lexeme with + (match lookup_ligatures lexeme with | [] -> (* ligature not found, rollback and try default lexer *) Ulexing.rollback lexbuf; k lexbuf - | ligs -> (* ligatures found, use the default one *) - let default_lig = List.hd (List.rev ligs) in + | default_lig :: _ -> (* ligatures found, use the default one *) return_symbol lexbuf default_lig) | eof -> return_eoi lexbuf | _ -> (* not a ligature, rollback and try default lexer *) diff --git a/helm/ocaml/cic_notation/cicNotationLexer.mli b/helm/ocaml/cic_notation/cicNotationLexer.mli index 765a554f4..cd5f0876d 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.mli +++ b/helm/ocaml/cic_notation/cicNotationLexer.mli @@ -41,5 +41,8 @@ val level2_meta_lexer: (string * string) Token.glexer val add_level2_ast_keyword: string -> unit (** non idempotent *) val remove_level2_ast_keyword: string -> unit (** non idempotent *) -(* val lookup_ligatures: string -> string list *) +(** {2 Ligatures} *) + +val is_ligature_char: char -> bool +val lookup_ligatures: string -> string list -- 2.39.2