diff options
| author | Emilio Jesus Gallego Arias | 2018-10-06 17:54:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-29 01:25:21 +0100 |
| commit | 06979f87959866e6ed1214e745893dcd2e8ddbb3 (patch) | |
| tree | 458274f8a8afedc314535db28e0936b7fe3bec3c /gramlib/token.ml | |
| parent | 665146168720c094ce4fbb3d7d044d9904099f95 (diff) | |
[gramlib] Original Import from Camlp5 repos.
Diffstat (limited to 'gramlib/token.ml')
| -rw-r--r-- | gramlib/token.ml | 37 |
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; |
