diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-09 16:33:21 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-09 16:35:49 +0200 |
commit | a66b57ba4bba866bb626bde2b6fe3b762347eb3e (patch) | |
tree | 7e78979db8010c5221352cb7fcbcc12a8be3db62 /toplevel/metasyntax.ml | |
parent | b43956fe19177a178dfbcef0b173ebada5060973 (diff) |
Rename Lexer -> CLexer.
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r-- | toplevel/metasyntax.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 2ccd27acb..c33726550 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -31,7 +31,7 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = Lexer.add_keyword s +let cache_token (_,s) = CLexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with @@ -428,7 +428,7 @@ let rec interp_list_parser hd = function (* To protect alphabetic tokens and quotes from being seen as variables *) let quote_notation_token x = let n = String.length x in - let norm = Lexer.is_ident x in + let norm = CLexer.is_ident x in if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'" else x @@ -436,7 +436,7 @@ let rec raw_analyze_notation_tokens = function | [] -> [] | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl | String "_" :: _ -> error "_ must be quoted." - | String x :: sl when Lexer.is_ident x -> + | String x :: sl when CLexer.is_ident x -> NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl | String s :: sl -> Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl @@ -725,7 +725,7 @@ let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - Lexer.add_keyword k; + CLexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] @@ -734,7 +734,7 @@ let rec define_keywords_aux = function let define_keywords = function | GramConstrTerminal(IDENT k)::l -> Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); - Lexer.add_keyword k; + CLexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -763,12 +763,12 @@ let make_production etyps symbols = let typ = List.assoc m etyps in distribute [GramConstrNonTerminal (typ, Some m)] ll | Terminal s -> - distribute [GramConstrTerminal (Lexer.terminal s)] ll + distribute [GramConstrTerminal (CLexer.terminal s)] ll | Break _ -> ll | SProdList (x,sl) -> let tkl = List.flatten - (List.map (function Terminal s -> [Lexer.terminal s] + (List.map (function Terminal s -> [CLexer.terminal s] | Break _ -> [] | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in match List.assoc x etyps with |