aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--dev/printers.mllib2
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/grammar.mllib2
-rw-r--r--parsing/cLexer.ml4 (renamed from parsing/lexer.ml4)0
-rw-r--r--parsing/cLexer.mli (renamed from parsing/lexer.mli)0
-rw-r--r--parsing/compat.ml42
-rw-r--r--parsing/egramcoq.ml6
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/parsing.mllib2
-rw-r--r--parsing/pcoq.ml44
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/coqloop.ml2
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/metasyntax.ml14
-rw-r--r--toplevel/vernac.ml8
20 files changed, 31 insertions, 31 deletions
diff --git a/.gitignore b/.gitignore
index 3adb9c67c..6d843661f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -127,7 +127,7 @@ grammar/tacextend.ml
grammar/vernacextend.ml
grammar/argextend.ml
parsing/pcoq.ml
-parsing/lexer.ml
+parsing/cLexer.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 ad9a5d75e..e054c1bc7 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -151,7 +151,7 @@ States
Genprint
Tok
-Lexer
+CLexer
Ppextend
Pputils
Ppannotation
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index cb0f7d2d3..b3c71a703 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
- Lexer.add_keyword s;
+ CLexer.add_keyword s;
GramTerminal s
] ]
;
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 71e5b8ae2..1864fae5f 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -50,7 +50,7 @@ Constrexpr_ops
Compat
Tok
-Lexer
+CLexer
Pcoq
G_prim
G_tactic
diff --git a/parsing/lexer.ml4 b/parsing/cLexer.ml4
index 5d96873f3..5d96873f3 100644
--- a/parsing/lexer.ml4
+++ b/parsing/cLexer.ml4
diff --git a/parsing/lexer.mli b/parsing/cLexer.mli
index 24b0ec847..24b0ec847 100644
--- a/parsing/lexer.mli
+++ b/parsing/cLexer.mli
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 17038ab5f..1481c31f4 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -135,7 +135,7 @@ let to_coq_position = function
END
-(** Signature of Lexer *)
+(** Signature of CLexer *)
IFDEF CAMLP5 THEN
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index b0bbdd813..4c7743303 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 * Lexer.frozen_t
+type frozen_t = (int * all_grammar_command) list * CLexer.frozen_t
-let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
+let freeze _ : frozen_t = (!grammar_state, CLexer.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;
- Lexer.unfreeze lex;
+ CLexer.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 5edb7b808..73b088b46 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -29,7 +29,7 @@ let constr_kw =
"Prop"; "Set"; "Type"; ".("; "_"; "..";
"`{"; "`("; "{|"; "|}" ]
-let _ = List.iter Lexer.add_keyword constr_kw
+let _ = List.iter CLexer.add_keyword constr_kw
let mk_cast = function
(c,(_,None)) -> c
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 5297c163b..20fbccb2d 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 Lexer.add_keyword prim_kw
+let _ = List.iter CLexer.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 2a00a1764..8f3d04eeb 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 Lexer.add_keyword tactic_kw
+let _ = List.iter CLexer.add_keyword tactic_kw
let err () = raise Stream.Failure
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f3766a7d7..b19ad8807 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 Lexer.add_keyword vernac_kw
+let _ = List.iter CLexer.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/parsing.mllib b/parsing/parsing.mllib
index a0cb83193..0e1c79c91 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,6 @@
Tok
Compat
-Lexer
+CLexer
Pcoq
Egramml
Egramcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 28dc74e81..f01e25c61 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 (Lexer)
+module G = GrammarMake (CLexer)
(* 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 (Lexer.terminal s)
+let gram_token_of_string s = gram_token_of_token (CLexer.terminal s)
let camlp4_verbosity silent f x =
let a = !warning_verbose in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5ecc46d67..a7acdf759 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 Lexer.is_keyword s then s^"0" else s in
+ let s = if CLexer.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 600683d35..d8ee5d90d 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 ".")
- | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
+ | CLexer.Error.E err -> hov 0 (str (CLexer.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 063ed8964..040c33924 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 _ | Lexer.Error.E _ -> discard_to_dot ()
+ | Compat.Token.Error _ | CLexer.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 9e1a76bbd..08b38a703 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 = Lexer.location_table () in
+ let coqdoc_init_state = CLexer.location_table () in
List.iter
(fun vf ->
States.unfreeze init_state;
- Lexer.restore_location_table coqdoc_init_state;
+ CLexer.restore_location_table coqdoc_init_state;
compile_file vf)
(List.rev l)
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
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7c4920dfb..a5f502503 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 = Lexer.com_state() in
+ let cs = CLexer.com_state() in
(* end translator state *)
- let coqdocstate = Lexer.location_table () in
+ let coqdocstate = CLexer.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;
- Lexer.restore_com_state cs;
- Lexer.restore_location_table coqdocstate
+ CLexer.restore_com_state cs;
+ CLexer.restore_location_table coqdocstate
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 00:39:15 +0000