diff options
Diffstat (limited to 'gramlib/plexing.mli')
| -rw-r--r-- | gramlib/plexing.mli | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 521eba7446..0c190af635 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -15,7 +15,7 @@ and location_function = int -> Loc.t (** The type of a function giving the location of a token in the source from the token number in the stream (starting from zero). *) -module type Lexer = sig +module type S = sig type te type 'c pattern val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option @@ -25,4 +25,15 @@ module type Lexer = sig val tok_removing : 'c pattern -> unit val tok_match : 'c pattern -> te -> 'c val tok_text : 'c pattern -> string + + (* State for the comments, at some point we should make it functional *) + module State : sig + type t + val init : unit -> t + val set : t -> unit + val get : unit -> t + val drop : unit -> unit + val get_comments : t -> ((int * int) * string) list + end + end |