diff options
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | dev/printers.mllib | 2 | ||||
-rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
-rw-r--r-- | grammar/grammar.mllib | 2 | ||||
-rw-r--r-- | parsing/compat.ml4 | 2 | ||||
-rw-r--r-- | parsing/egramcoq.ml | 6 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
-rw-r--r-- | parsing/lexer.ml4 (renamed from parsing/cLexer.ml4) | 0 | ||||
-rw-r--r-- | parsing/lexer.mli (renamed from parsing/cLexer.mli) | 0 | ||||
-rw-r--r-- | parsing/parsing.mllib | 2 | ||||
-rw-r--r-- | parsing/pcoq.ml4 | 4 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | toplevel/cerrors.ml | 2 | ||||
-rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 14 | ||||
-rw-r--r-- | toplevel/vernac.ml | 8 |
20 files changed, 31 insertions, 31 deletions
diff --git a/.gitignore b/.gitignore index 3f9856916..7efa76130 100644 --- a/.gitignore +++ b/.gitignore @@ -127,7 +127,7 @@ grammar/tacextend.ml grammar/vernacextend.ml grammar/argextend.ml parsing/pcoq.ml -parsing/cLexer.ml +parsing/lexer.ml plugins/setoid_ring/newring.ml plugins/field/field.ml plugins/nsatz/nsatz.ml diff --git a/dev/printers.mllib b/dev/printers.mllib index e054c1bc7..ad9a5d75e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -151,7 +151,7 @@ States Genprint Tok -CLexer +Lexer Ppextend Pputils Ppannotation diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index b3c71a703..cb0f7d2d3 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -287,7 +287,7 @@ EXTEND GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then - CLexer.add_keyword s; + Lexer.add_keyword s; GramTerminal s ] ] ; diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 1864fae5f..71e5b8ae2 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -50,7 +50,7 @@ Constrexpr_ops Compat Tok -CLexer +Lexer Pcoq G_prim G_tactic diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 1481c31f4..17038ab5f 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -135,7 +135,7 @@ let to_coq_position = function END -(** Signature of CLexer *) +(** Signature of Lexer *) IFDEF CAMLP5 THEN diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 4c7743303..b0bbdd813 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -317,9 +317,9 @@ let recover_constr_grammar ntn prec = (* Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing grammar rules. *) -type frozen_t = (int * all_grammar_command) list * CLexer.frozen_t +type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t -let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) +let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) @@ -335,7 +335,7 @@ let unfreeze (grams, lex) = remove_grammars n; remove_levels n; grammar_state := common; - CLexer.unfreeze lex; + Lexer.unfreeze lex; List.iter extend_grammar (List.rev_map snd redo) (** No need to provide an init function : the grammar state is diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 73b088b46..5edb7b808 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -29,7 +29,7 @@ let constr_kw = "Prop"; "Set"; "Type"; ".("; "_"; ".."; "`{"; "`("; "{|"; "|}" ] -let _ = List.iter CLexer.add_keyword constr_kw +let _ = List.iter Lexer.add_keyword constr_kw let mk_cast = function (c,(_,None)) -> c diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 20fbccb2d..5297c163b 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -15,7 +15,7 @@ open Pcoq open Pcoq.Prim let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] -let _ = List.iter CLexer.add_keyword prim_kw +let _ = List.iter Lexer.add_keyword prim_kw let local_make_qualid l id = make_qualid (DirPath.make l) id diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8f3d04eeb..2a00a1764 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -25,7 +25,7 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta] let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw +let _ = List.iter Lexer.add_keyword tactic_kw let err () = raise Stream.Failure diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b19ad8807..f3766a7d7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -27,7 +27,7 @@ open Pcoq.Vernac_ open Pcoq.Module let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw +let _ = List.iter Lexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) diff --git a/parsing/cLexer.ml4 b/parsing/lexer.ml4 index 5d96873f3..5d96873f3 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/lexer.ml4 diff --git a/parsing/cLexer.mli b/parsing/lexer.mli index 24b0ec847..24b0ec847 100644 --- a/parsing/cLexer.mli +++ b/parsing/lexer.mli diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 0e1c79c91..a0cb83193 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,6 +1,6 @@ Tok Compat -CLexer +Lexer Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f01e25c61..28dc74e81 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -18,7 +18,7 @@ open Tok (* necessary for camlp4 *) (** The parser of Coq *) -module G = GrammarMake (CLexer) +module G = GrammarMake (Lexer) (* TODO: this is a workaround, since there isn't such [warning_verbose] in new camlp4. In camlp5, this ref @@ -51,7 +51,7 @@ ELSE | tok -> Stoken ((=) tok, to_string tok) END -let gram_token_of_string s = gram_token_of_token (CLexer.terminal s) +let gram_token_of_string s = gram_token_of_token (Lexer.terminal s) let camlp4_verbosity silent f x = let a = !warning_verbose in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a7acdf759..5ecc46d67 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -491,7 +491,7 @@ let interp_fresh_id ist env sigma l = String.concat "" (List.map (function | ArgArg s -> s | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in - let s = if CLexer.is_keyword s then s^"0" else s in + let s = if Lexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index d8ee5d90d..600683d35 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -35,7 +35,7 @@ let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) + | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 040c33924..063ed8964 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -288,7 +288,7 @@ let rec discard_to_dot () = try Gram.entry_parse parse_to_dot top_buffer.tokens with - | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot () + | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot () | End_of_input -> raise End_of_input | e when Errors.noncritical e -> () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 08b38a703..9e1a76bbd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -230,11 +230,11 @@ let compile_files () = | [vf] -> compile_file vf (* One compilation : no need to save init state *) | l -> let init_state = States.freeze ~marshallable:`No in - let coqdoc_init_state = CLexer.location_table () in + let coqdoc_init_state = Lexer.location_table () in List.iter (fun vf -> States.unfreeze init_state; - CLexer.restore_location_table coqdoc_init_state; + Lexer.restore_location_table coqdoc_init_state; compile_file vf) (List.rev l) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c33726550..2ccd27acb 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -31,7 +31,7 @@ open Nameops (**********************************************************************) (* Tokens *) -let cache_token (_,s) = CLexer.add_keyword s +let cache_token (_,s) = Lexer.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 = CLexer.is_ident x in + let norm = Lexer.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 CLexer.is_ident x -> + | String x :: sl when Lexer.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"); - CLexer.add_keyword k; + Lexer.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"); - CLexer.add_keyword k; + Lexer.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 (CLexer.terminal s)] ll + distribute [GramConstrTerminal (Lexer.terminal s)] ll | Break _ -> ll | SProdList (x,sl) -> let tkl = List.flatten - (List.map (function Terminal s -> [CLexer.terminal s] + (List.map (function Terminal s -> [Lexer.terminal s] | Break _ -> [] | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in match List.assoc x etyps with diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a5f502503..7c4920dfb 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -164,17 +164,17 @@ let save_translator_coqdoc () = (* translator state *) let ch = !chan_beautify in let cl = !Pp.comments in - let cs = CLexer.com_state() in + let cs = Lexer.com_state() in (* end translator state *) - let coqdocstate = CLexer.location_table () in + let coqdocstate = Lexer.location_table () in ch,cl,cs,coqdocstate let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Pp.comments := cl; - CLexer.restore_com_state cs; - CLexer.restore_location_table coqdocstate + Lexer.restore_com_state cs; + Lexer.restore_location_table coqdocstate (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) |