From 912eaf40d4efd29b7e3489d51c55b8b79206df79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 Mar 2019 11:42:17 +0100
Subject: [parsing] Split Tok.t into Tok.t and Tok.pattern

Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals

Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t

Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
---
 gramlib/plexing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'gramlib/plexing.ml')

diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index c294923a85..6da06f147f 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -2,7 +2,7 @@
 (* plexing.ml,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-type pattern = string * string
+type pattern = string * string option
 
 type location_function = int -> Loc.t
 type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
-- 
cgit v1.2.3