aboutsummaryrefslogtreecommitdiff
path: root/gramlib/plexing.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-02-21 14:18:37 -0500
committerEmilio Jesus Gallego Arias2020-03-25 23:45:01 -0400
commitef3079e22fa7941d3335d7779c840e8d2d2bde39 (patch)
tree6f524c811c79c1e3271b2c86ce3b29275b876075 /gramlib/plexing.ml
parent9847448b5f9dbf32806decf676f415d584a2cddb (diff)
[parsing] Move comments lexer extensions to base lexer interface
This makes sense as a step towards a more functional handling of the state.
Diffstat (limited to 'gramlib/plexing.ml')
-rw-r--r--gramlib/plexing.ml13
1 files changed, 12 insertions, 1 deletions
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index e881ab3350..ce3e38ff08 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -5,7 +5,7 @@
type location_function = int -> Loc.t
type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
-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
@@ -15,4 +15,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