diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-11 19:42:14 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 18:16:22 +0100 |
commit | 2a64471512ee7dcd6d6c65cd5a792344628616f0 (patch) | |
tree | 9c98439db32ece160fd08304bfc4f1b5a63584e2 /parsing/pcoq.ml | |
parent | 893f8a3a3c573ab6b11cc3938cc67ccdc1b6b4ea (diff) |
[toplevel] Move beautify to its own pass.
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r-- | parsing/pcoq.ml | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7a51908d9..fec26f941 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -88,7 +88,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 +107,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 +132,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 |