aboutsummaryrefslogtreecommitdiff
path: root/gramlib/plexing.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-03-31 00:48:42 +0200
committerPierre-Marie Pédrot2020-03-31 00:48:42 +0200
commite2f0814688511be93659c2258b91248698f18d4a (patch)
tree06c1860a6e5b45ee154e45bfbddfff228ac22cdd /gramlib/plexing.mli
parent8c85a8651605dd82ce2223a28ca38f31359a88bd (diff)
parent5c9f318f5f1b6e85b03bba9450ac059377be54fc (diff)
Merge PR #11647: [rfc] Consolidation of parsing interfaces
Ack-by: SkySkimmer Reviewed-by: ppedrot
Diffstat (limited to 'gramlib/plexing.mli')
-rw-r--r--gramlib/plexing.mli13
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