diff options
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7a51908d9..258c4bb11 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) open CErrors @@ -88,7 +90,9 @@ module type S = val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit - val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b + + val comment_state : coq_parsable -> ((int * int) * string) list + val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a @@ -105,6 +109,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list + type coq_parsable = parsable * CLexer.lexer_state ref let parsable ?(file=Loc.ToplevelInput) c = @@ -129,15 +134,8 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in Loc.raise ~loc e - let with_parsable (p,state) f x = - CLexer.set_lexer_state !state; - try - let a = f x in - state := CLexer.get_lexer_state (); - a - with e -> - CLexer.drop_lexer_state (); - raise e + let comment_state (p,state) = + CLexer.get_comment_state !state let entry_print ft x = Entry.print ft x @@ -444,6 +442,7 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" + let univ_decl = Gram.entry_create "Prim.univ_decl" let ident_decl = Gram.entry_create "Prim.ident_decl" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" |