- hExtlib: added debugging information for split_nth

[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 bbc901dab7db3e2f139e37e6e65639efe1d2abd4..b13c7887f3b07acde439ce7854ce5a0627dc070c 100644 (file)
--- a/helm/software/components/content_pres/cicNotationLexer.ml
+++ b/helm/software/components/content_pres/cicNotationLexer.ml
@@ -52,6 +52,8 @@ let regexp we_proved = "we" utf8_blank+ "proved"
 let regexp we_have = "we" utf8_blank+ "have"
 let regexp let_rec = "let" utf8_blank+ "rec" 
 let regexp let_corec = "let" utf8_blank+  "corec"
+let regexp nlet_rec = "nlet" utf8_blank+ "rec" 
+let regexp nlet_corec = "nlet" utf8_blank+  "corec"
 let regexp ident_decoration = '\'' | '?' | '`'
 let regexp ident_cont = ident_letter | xml_digit | '_'
 let regexp ident = ident_letter ident_cont* ident_decoration*
@@ -88,7 +90,8 @@ let level1_layouts =
   [ "sub"; "sup";
     "below"; "above";
     "over"; "atop"; "frac";
-    "sqrt"; "root"
+    "sqrt"; "root"; "mstyle" ; "mpadded"; "maction"
+
   ]
 
 let level1_keywords =
@@ -96,7 +99,7 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number"; "mstyle" ; "mpadded"
+    "term"; "ident"; "number";
   ] @ level1_layouts
 
 let level2_meta_keywords =
@@ -131,9 +134,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' '_' '-' ''' ]+
@@ -285,6 +286,8 @@ and level2_ast_token =
   lexer
   | let_rec -> return lexbuf ("LETREC","")
   | let_corec -> return lexbuf ("LETCOREC","")
+  | nlet_rec -> return lexbuf ("NLETREC","")
+  | nlet_corec -> return lexbuf ("NLETCOREC","")
   | we_proved -> return lexbuf ("WEPROVED","")
   | we_have -> return lexbuf ("WEHAVE","")
   | utf8_blank+ -> ligatures_token level2_ast_token lexbuf