aboutsummaryrefslogtreecommitdiff
path: root/parsing/cLexer.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-05 18:51:30 +0100
committerEmilio Jesus Gallego Arias2018-11-05 18:51:30 +0100
commitefe60d3c1b09bc059053b7383e068ddc05248dac (patch)
treecef40d35eb429346ab6649ce9d4985990a337623 /parsing/cLexer.ml
parent56a654cc248b2be6e85b7f8f8f88efe289c704d5 (diff)
parentb255fe1699be4e5dc067c23c92239ad1c67424f9 (diff)
Merge PR #8899: Remove the deprecated Token module and port the corresponding code.
Diffstat (limited to 'parsing/cLexer.ml')
-rw-r--r--parsing/cLexer.ml12
1 files changed, 6 insertions, 6 deletions
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 *)