let regexp number = xml_digit+
let regexp utf8_blank = " " | "\r\n" | "\n" | "\t" | [160] (* this is a nbsp *)
+let regexp percentage =
+ ('-' | "") [ '0' - '9' ] + '%'
+let regexp floatwithunit =
+ ('-' | "") [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" )
+let regexp color = "#" [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f'
+'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
+[ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
(* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
(* let regexp ident_letter = xml_letter *)
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"
+let regexp let_corec = "let" utf8_blank+ "corec"
let regexp ident_decoration = '\'' | '?' | '`'
let regexp ident_cont = ident_letter | xml_digit | '_'
let regexp ident = ident_letter ident_cont* ident_decoration*
[ "sub"; "sup";
"below"; "above";
"over"; "atop"; "frac";
- "sqrt"; "root"
+ "sqrt"; "root"; "mstyle" ; "mpadded"; "maction"
+
]
let level1_keywords =
"break";
"list0"; "list1"; "sep";
"opt";
- "term"; "ident"; "number"
+ "term"; "ident"; "number";
] @ level1_layouts
let level2_meta_keywords =
- [ "if"; "then"; "else";
+ [ "if"; "then"; "elCicNotationParser.se";
"fold"; "left"; "right"; "rec";
"fail";
"default";
]
(* (string, unit) Hashtbl.t, to exploit multiple bindings *)
-let level2_ast_keywords = Hashtbl.create 23
-let _ =
- List.iter (fun k -> Hashtbl.add level2_ast_keywords k ())
- [ "CProp"; "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match";
- "with"; "in"; "and"; "to"; "as"; "on"; "return" ]
+let initial_level2_ast_keywords () = Hashtbl.create 23;;
+
+let level2_ast_keywords = ref (initial_level2_ast_keywords ())
+
+let initialize_keywords () =
+ List.iter (fun k -> Hashtbl.add !level2_ast_keywords k ())
+ [ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
+ "with"; "in"; "and"; "to"; "as"; "on"; "return"; "done" ]
+;;
-let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k ()
-let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k
+let _ = initialize_keywords ();;
+
+let add_level2_ast_keyword k = Hashtbl.add !level2_ast_keywords k ()
+let remove_level2_ast_keyword k = Hashtbl.remove !level2_ast_keywords k
(* (string, int) Hashtbl.t, with multiple bindings.
* int is the unicode codepoint *)
let ligatures = Hashtbl.create 23
+
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' '_' '-' ''' ]+
and level2_ast_token =
lexer
+ | let_rec -> return lexbuf ("LETREC","")
+ | let_corec -> return lexbuf ("LETCOREC","")
+ | we_proved -> return lexbuf ("WEPROVED","")
+ | we_have -> return lexbuf ("WEHAVE","")
| utf8_blank+ -> ligatures_token level2_ast_token lexbuf
| meta ->
let s = Ulexing.utf8_lexeme lexbuf in
| placeholder -> return lexbuf ("PLACEHOLDER", "")
| ident ->
let lexeme = Ulexing.utf8_lexeme lexbuf in
- if Hashtbl.mem level2_ast_keywords lexeme then
+ if Hashtbl.mem !level2_ast_keywords lexeme then
return lexbuf ("", lexeme)
else
return lexbuf ("IDENT", lexeme)
else
return lexbuf ("IDENT", s)
end
+ | color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf)
+ | percentage ->
+ return lexbuf ("PERCENTAGE", Ulexing.utf8_lexeme lexbuf)
+ | 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))
(* API implementation *)
-let level1_pattern_lexer = mk_lexer level1_pattern_token
-let level2_ast_lexer = mk_lexer level2_ast_token
-let level2_meta_lexer = mk_lexer level2_meta_token
-
-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 initial_level1_pattern_lexer () = mk_lexer level1_pattern_token
+let initial_level2_ast_lexer () = mk_lexer level2_ast_token
+let initial_level2_meta_lexer () = mk_lexer level2_meta_token
+
+
+let level1_pattern_lexer_ref = ref (initial_level1_pattern_lexer ())
+let level2_ast_lexer_ref = ref (initial_level2_ast_lexer ())
+let level2_meta_lexer_ref = ref (initial_level2_meta_lexer ())
+
+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 history = ref [];;
+
+let push () =
+ history :=
+ (!level2_ast_keywords,!level1_pattern_lexer_ref,
+ !level2_ast_lexer_ref,!level2_meta_lexer_ref) :: !history;
+ level2_ast_keywords := initial_level2_ast_keywords ();
+ initialize_keywords ();
+ level1_pattern_lexer_ref := initial_level1_pattern_lexer ();
+ level2_ast_lexer_ref := initial_level2_ast_lexer ();
+ level2_meta_lexer_ref := initial_level2_meta_lexer ();
+;;
+
+let pop () =
+ match !history with
+ | [] -> assert false
+ | (kwd,pl,al,ml) :: tl ->
+ level2_ast_keywords := kwd;
+ level1_pattern_lexer_ref := pl;
+ level2_ast_lexer_ref := al;
+ level2_meta_lexer_ref := ml;
+ history := tl
+;;
projects / helm.git / blobdiff