Remove the deprecated Token module and port the corresponding code.

5 files changed, 8 insertions, 101 deletions

diff --git a/gramlib/token.ml b/gramlib/token.ml
deleted file mode 100644
index 77c737b880..0000000000
--- a/gramlib/token.ml
+++ /dev/null
@@ -1,37 +0,0 @@
-(* camlp5r *)
-(* token.ml,v *)
-(* Copyright (c) INRIA 2007-2017 *)
-
-type pattern = Plexing.pattern
-
-exception Error of string
-
-type location = Ploc.t
-type location_function = int -> location
-type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
-
-type 'te glexer =
-  'te Plexing.lexer =
-    { tok_func : 'te lexer_func;
-      tok_using : pattern -> unit;
-      tok_removing : pattern -> unit;
-      mutable tok_match : pattern -> 'te -> string;
-      tok_text : pattern -> string;
-      mutable tok_comm : location list option }
-
-let make_loc = Ploc.make_unlined
-let dummy_loc = Ploc.dummy
-
-let make_stream_and_location = Plexing.make_stream_and_location
-let lexer_func_of_parser = Plexing.lexer_func_of_parser
-let lexer_func_of_ocamllex = Plexing.lexer_func_of_ocamllex
-
-let eval_char = Plexing.eval_char
-let eval_string = Plexing.eval_string
-
-let lexer_text = Plexing.lexer_text
-let default_match = Plexing.default_match
-
-let line_nb = Plexing.line_nb
-let bol_pos = Plexing.bol_pos
-let restore_lexing_info = Plexing.restore_lexing_info
diff --git a/gramlib/token.mli b/gramlib/token.mli
deleted file mode 100644
index c1de5cefff..0000000000
--- a/gramlib/token.mli
+++ /dev/null
@@ -1,56 +0,0 @@
-(* camlp5r *)
-(* token.mli,v *)
-(* Copyright (c) INRIA 2007-2017 *)
-
-(** Module deprecated since Camlp5 version 5.00. Use now module Plexing.
-    Compatibility assumed. *)
-
-type pattern = Plexing.pattern
-
-exception Error of string
-    (** Use now [Plexing.Error] *)
-
-type 'te glexer =
-  'te Plexing.lexer =
-    { tok_func : 'te Plexing.lexer_func;
-      tok_using : pattern -> unit;
-      tok_removing : pattern -> unit;
-      mutable tok_match : pattern -> 'te -> string;
-      tok_text : pattern -> string;
-      mutable tok_comm : Ploc.t list option }
-
-type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
-and location_function = int -> Ploc.t
-
-val lexer_text : pattern -> string
-   (** Use now [Plexing.lexer_text] *)
-val default_match : pattern -> string * string -> string
-   (** Use now [Plexing.default_match] *)
-
-val lexer_func_of_parser :
-  (char Stream.t * int ref * int ref -> 'te * Ploc.t) -> 'te lexer_func
-   (** Use now [Plexing.lexer_func_of_parser] *)
-val lexer_func_of_ocamllex : (Lexing.lexbuf -> 'te) -> 'te lexer_func
-   (** Use now [Plexing.lexer_func_of_ocamllex] *)
-
-val make_stream_and_location :
-  (unit -> 'te * Ploc.t) -> 'te Stream.t * location_function
-   (** Use now [Plexing.make_stream_and_location] *)
-
-val eval_char : string -> char
-   (** Use now [Plexing.eval_char] *)
-val eval_string : Ploc.t -> string -> string
-   (** Use now [Plexing.eval_string] *)
-
-val restore_lexing_info : (int * int) option ref
-   (** Use now [Plexing.restore_lexing_info] *)
-val line_nb : int ref ref
-   (** Use now [Plexing.line_nb] *)
-val bol_pos : int ref ref
-   (** Use now [Plexing.bol_pos] *)
-
-(* deprecated since version 4.08 *)
-
-type location = Ploc.t
-val make_loc : int * int -> Ploc.t
-val dummy_loc : Ploc.t
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 2230dfc47c..619718f723 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -767,15 +767,15 @@ let func cs =
   (ts, loct_func loct)
 
 let lexer = {
-  Token.tok_func = func;
-  Token.tok_using =
+  Plexing.tok_func = func;
+  Plexing.tok_using =
     (fun pat -> match Tok.of_pattern pat with
        | KEYWORD s -> add_keyword s
        | _ -> ());
-  Token.tok_removing = (fun _ -> ());
-  Token.tok_match = Tok.match_pattern;
-  Token.tok_comm = None;
-  Token.tok_text = token_text }
+  Plexing.tok_removing = (fun _ -> ());
+  Plexing.tok_match = Tok.match_pattern;
+  Plexing.tok_comm = None;
+  Plexing.tok_text = token_text }
 
 (** Terminal symbols interpretation *)
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 59a464a22e..cbc5c124c8 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -255,7 +255,7 @@ let rec discard_to_dot () =
   try
     Pcoq.Entry.parse parse_to_dot top_buffer.tokens
   with
-    | Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
+    | Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot ()
     | Stm.End_of_input -> raise Stm.End_of_input
     | e when CErrors.noncritical e -> ()
 
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index b37fce645a..e6803443b3 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -29,7 +29,7 @@ exception EvaluatedError of Pp.t * exn option
 let explain_exn_default = function
   (* Basic interaction exceptions *)
   | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
+  | Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | 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.")