diff options
Diffstat (limited to 'parsing/cLexer.mli')
| -rw-r--r-- | parsing/cLexer.mli | 60 |
1 files changed, 44 insertions, 16 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** 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 : 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 |