diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 14:18:37 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:01 -0400 |
| commit | ef3079e22fa7941d3335d7779c840e8d2d2bde39 (patch) | |
| tree | 6f524c811c79c1e3271b2c86ce3b29275b876075 /gramlib/grammar.mli | |
| parent | 9847448b5f9dbf32806decf676f415d584a2cddb (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/grammar.mli')
| -rw-r--r-- | gramlib/grammar.mli | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 16e147de3b..0872321da0 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -17,18 +17,6 @@ (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) -module type GLexerType = sig - include Plexing.Lexer - - 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 type norec type mayrec @@ -130,5 +118,4 @@ end type (instead of (string * string)); the module parameter must specify a way to show them as (string * string) *) -module GMake (L : GLexerType) : - S with type te = L.te and type 'c pattern = 'c L.pattern +module GMake (L : Plexing.S) : S with type te = L.te and type 'c pattern = 'c L.pattern |