From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- parsing/cLexer.mli | 60 +++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 44 insertions(+), 16 deletions(-) (limited to 'parsing/cLexer.mli') diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index e0fdf8cb..a14f08d9 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -1,32 +1,60 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 : Loc.source -> lexer_state +val set_lexer_state : lexer_state -> unit +val get_lexer_state : unit -> lexer_state +val release_lexer_state : unit -> lexer_state +[@@ocaml.deprecated "Use get_lexer_state"] +val drop_lexer_state : unit -> unit +val get_comment_state : lexer_state -> ((int * int) * string) list -- cgit v1.2.3