Matitaweb:

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

diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml
index 3c84e0bb5056f94e1f2e9bd138f4185c32b609e3..b7451bc780c8925f539aa72f589afdf764d9cf6c 100644 (file)
--- a/matitaB/components/content_pres/cicNotationLexer.ml
+++ b/matitaB/components/content_pres/cicNotationLexer.ml
@@ -130,11 +130,11 @@ let level1_keywords =
     "break";
     "list0"; "list1"; "sep";
     "opt";
-    "term"; "ident"; "number";
+    "term"; "ident"; "number"; "ref"
   ] @ level1_layouts
 
 let level2_meta_keywords =
-  [ "if"; "then"; "elCicNotationParser.se";
+  [ "if"; "then"; "else";
     "fold"; "left"; "right"; "rec";
     "fail";
     "default";
@@ -463,10 +463,14 @@ let rec level1_pattern_token =
   lexer
   | utf8_blank+ -> ligatures_token level1_pattern_token lexbuf
   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
-  | hreftag -> return lexbuf ("ATAG", "")
+(*  | hreftag -> return lexbuf ("ATAG", "")
   | hrefclose -> return lexbuf ("ATAGEND","")
   | generictag 
-  | closetag -> ligatures_token level1_pattern_token lexbuf
+  | closetag -> ligatures_token level1_pattern_token lexbuf *)
+  | qkeyword ->
+      return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
+  | csymbol -> prerr_endline ("lexing csymbol " ^ (Ulexing.utf8_lexeme lexbuf));
+      return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
   | ident -> handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
   | pident-> handle_keywords lexbuf (fun x->List.mem x level1_keywords) "PIDENT" 
@@ -476,8 +480,6 @@ let rec level1_pattern_token =
   | floatwithunit -> 
       return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
-  | qkeyword ->
-      return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
   | '(' -> return lexbuf ("LPAREN", "")
   | ')' -> return lexbuf ("RPAREN", "")
   | eof -> return_eoi lexbuf