The substitution is now taken in account when printing sequents in the

[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml

diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml
index 11fcc4106d812e643df6f83151657612e8110fbd..ac3b1142252dda604e88ccde5c86b32af757865b 100644 (file)
--- 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" 
@@ -97,7 +88,8 @@ let level1_layouts =
   [ "sub"; "sup";
     "below"; "above";
     "over"; "atop"; "frac";
-    "sqrt"; "root"
+    "sqrt"; "root"; "mstyle" ; "mpadded"; "maction"
+
   ]
 
 let level1_keywords =
@@ -105,7 +97,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"; "mstyle" ; "mpadded"
+    "term"; "ident"; "number";
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -140,9 +132,7 @@ let _ =
   List.iter
     (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
     [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
-      ("<=", <:unicode<leq>>);  (">=", <:unicode<geq>>);
-      ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
-      ("==", <:unicode<equiv>>);
+      (":=", <:unicode<def>>);
     ]
 
 let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
@@ -378,14 +368,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 () =