X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=ac3b1142252dda604e88ccde5c86b32af757865b;hb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;hp=bbf7de133addba6e2e2cb93a60d6ffda753f56ba;hpb=fd93fa0155994b70482e0f07d8e45c238cce835d;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index bbf7de133..ac3b11422 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -31,6 +31,13 @@ exception Error of int * int * string 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 *) @@ -41,19 +48,10 @@ 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" ' '+ "proved" -let regexp we_have = "we" ' '+ "have" -let regexp let_rec = "let" ' '+ "rec" -let regexp let_corec = "let" ' '+ "corec" +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* @@ -90,7 +88,8 @@ let level1_layouts = [ "sub"; "sup"; "below"; "above"; "over"; "atop"; "frac"; - "sqrt"; "root" + "sqrt"; "root"; "mstyle" ; "mpadded"; "maction" + ] let level1_keywords = @@ -98,11 +97,11 @@ 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"; @@ -110,25 +109,30 @@ let level2_meta_keywords = ] (* (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 ()) +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>); ("=>", <:unicode>); - ("<=", <:unicode>); (">=", <:unicode>); - ("<>", <:unicode>); (":=", <:unicode>); - ("==", <:unicode>); + (":=", <:unicode>); ] let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ @@ -290,7 +294,7 @@ and level2_ast_token = | 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) @@ -333,6 +337,11 @@ and level1_pattern_token = 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)) @@ -346,14 +355,40 @@ let level2_ast_token = ligatures_token level2_ast_token (* 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 +;;