diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 03:22:22 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:55:41 +0200 |
commit | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch) | |
tree | 24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /parsing/cLexer.mli | |
parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) |
[camlpX] Remove camlp4 compat layer.
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
Diffstat (limited to 'parsing/cLexer.mli')
-rw-r--r-- | parsing/cLexer.mli | 48 |
1 files changed, 39 insertions, 9 deletions
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index e0fdf8cb5..1a1c302f2 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -6,27 +6,57 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This should be functional but it is not due to the interface *) val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool val keywords : unit -> CString.Set.t +type keyword_state +val set_keyword_state : keyword_state -> unit +val get_keyword_state : unit -> keyword_state + val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit -type frozen_t -val freeze : unit -> frozen_t -val unfreeze : frozen_t -> unit - val xml_output_comment : (string -> unit) Hook.t -(* Retrieve the comments lexed at a given location of the stream - currently being processeed *) -val extract_comments : int -> string list - val terminal : string -> Tok.t (** The lexer of Coq: *) -include Compat.LexerSig +(* modtype Grammar.GLexerType: sig + type te val + lexer : te Plexing.lexer + end + +where + + type lexer 'te = + { tok_func : lexer_func 'te; + tok_using : pattern -> unit; + tok_removing : pattern -> unit; + tok_match : pattern -> 'te -> string; + tok_text : pattern -> string; + tok_comm : mutable option (list location) } + *) +include Grammar.GLexerType with type te = Tok.t + +module Error : sig + type t + exception E of t + val to_string : t -> string +end + +(* Mainly for comments state, etc... *) +type lexer_state + +val init_lexer_state : string option -> lexer_state +val set_lexer_state : lexer_state -> unit +val release_lexer_state : unit -> lexer_state +val drop_lexer_state : unit -> unit + +(* Retrieve the comments lexed at a given location of the stream + currently being processeed *) +val extract_comments : int -> string list |