From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Jan 2009 16:07:48 +0000 (+0000)
Subject: removing (only from the interface) functions related to ligatures that now live in... 
X-Git-Tag: make_still_working~4289
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=279b11c00cdaacb4858e1c8dc6d05ea631bc1358;p=helm.git

removing (only from the interface) functions related to ligatures that now live in the GUI
---

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 11fcc4106..bbc901dab 100644
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -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 () =
diff --git a/helm/software/components/content_pres/cicNotationLexer.mli b/helm/software/components/content_pres/cicNotationLexer.mli
index f04575f5f..1edacd960 100644
--- a/helm/software/components/content_pres/cicNotationLexer.mli
+++ b/helm/software/components/content_pres/cicNotationLexer.mli
@@ -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