1 files changed, 18 insertions, 0 deletions
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
new file mode 100644
index 0000000000..f99a3c2480
--- /dev/null
+++ b/gramlib/plexing.ml
@@ -0,0 +1,18 @@
+(* camlp5r *)
+(* plexing.ml,v *)
+(* Copyright (c) INRIA 2007-2017 *)
+
+type pattern = string * string
+
+exception Error of string
+
+type location_function = int -> Loc.t
+type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
+
+type 'te lexer =
+  { tok_func : 'te lexer_func;
+    tok_using : pattern -> unit;
+    tok_removing : pattern -> unit;
+    tok_match : pattern -> 'te -> string;
+    tok_text : pattern -> string;
+  }