From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 4 Nov 2005 14:03:47 +0000 (+0000)
Subject: added ligatures expansion support functions
X-Git-Tag: V_0_7_2_3~132
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=921ba3b356400323b440a073a7030c5386d3b421;p=helm.git

added ligatures expansion support functions
---

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