aboutsummaryrefslogtreecommitdiff
path: root/gramlib/token.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-06 17:54:24 +0200
committerEmilio Jesus Gallego Arias2018-10-29 01:25:21 +0100
commit06979f87959866e6ed1214e745893dcd2e8ddbb3 (patch)
tree458274f8a8afedc314535db28e0936b7fe3bec3c /gramlib/token.ml
parent665146168720c094ce4fbb3d7d044d9904099f95 (diff)
[gramlib] Original Import from Camlp5 repos.
Diffstat (limited to 'gramlib/token.ml')
-rw-r--r--gramlib/token.ml37
1 files changed, 37 insertions, 0 deletions
diff --git a/gramlib/token.ml b/gramlib/token.ml
new file mode 100644
index 0000000000..9c1664ccd9
--- /dev/null
+++ b/gramlib/token.ml
@@ -0,0 +1,37 @@
+(* 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 lexer_func 'te = Stream.t char -> (Stream.t 'te * location_function);
+
+type glexer 'te = Plexing.lexer 'te ==
+ { tok_func : lexer_func 'te;
+ tok_using : pattern -> unit;
+ tok_removing : pattern -> unit;
+ tok_match : mutable pattern -> 'te -> string;
+ tok_text : pattern -> string;
+ tok_comm : mutable option (list location) }
+;
+
+value make_loc = Ploc.make_unlined;
+value dummy_loc = Ploc.dummy;
+
+value make_stream_and_location = Plexing.make_stream_and_location;
+value lexer_func_of_parser = Plexing.lexer_func_of_parser;
+value lexer_func_of_ocamllex = Plexing.lexer_func_of_ocamllex;
+
+value eval_char = Plexing.eval_char;
+value eval_string = Plexing.eval_string;
+
+value lexer_text = Plexing.lexer_text;
+value default_match = Plexing.default_match;
+
+value line_nb = Plexing.line_nb;
+value bol_pos = Plexing.bol_pos;
+value restore_lexing_info = Plexing.restore_lexing_info;