]> matita.cs.unibo.it Git - helm.git/commitdiff
removing (only from the interface) functions related to ligatures that now live in...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 Jan 2009 16:07:48 +0000 (16:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 Jan 2009 16:07:48 +0000 (16:07 +0000)
helm/software/components/content_pres/cicNotationLexer.ml
helm/software/components/content_pres/cicNotationLexer.mli

index 11fcc4106d812e643df6f83151657612e8110fbd..bbc901dab7db3e2f139e37e6e65639efe1d2abd4 100644 (file)
@@ -48,15 +48,6 @@ let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ]
 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 we_proved = "we" utf8_blank+ "proved"
 let regexp we_have = "we" utf8_blank+ "have"
 let regexp let_rec = "let" utf8_blank+ "rec" 
@@ -378,14 +369,6 @@ let level1_pattern_lexer () = !level1_pattern_lexer_ref
 let level2_ast_lexer () = !level2_ast_lexer_ref
 let level2_meta_lexer () = !level2_meta_lexer_ref 
 
-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 _ -> []
-;;
-
 let history = ref [];;
 
 let push () =
index f04575f5f7f7685ddd14c2d981bdc42bec428c7b..1edacd96097139dcfee979838ef9781d949414a0 100644 (file)
@@ -43,8 +43,5 @@ val remove_level2_ast_keyword: string -> unit (** non idempotent *)
 
 (** {2 Ligatures} *)
 
-val is_ligature_char: char -> bool
-val lookup_ligatures: string -> string list
-
 val push: unit -> unit
 val pop: unit -> unit