aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-05-31 13:33:01 +0200
committerPierre-Marie Pédrot2016-05-31 13:33:01 +0200
commit27dffdea5b46f6282c1584db0555213e744352fa (patch)
tree3f89cd9e8828f1ca1c8a1c10d74f020dcb7543f1 /toplevel
parentcb31cd671a0ef4da0cf834dad5b67776098bb0d1 (diff)
Revert "Rename Lexer -> CLexer."
This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
Diffstat (limited to 'toplevel')
-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
5 files changed, 15 insertions, 15 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index d8ee5d90da..600683d359 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 040c339249..063ed89643 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 08b38a7037..9e1a76bbd6 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 c33726550d..2ccd27acb9 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 a5f502503b..7c4920dfb8 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 *)