From ef29c0a927728d9cf4a45bc3c26d2393d753184e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 12:24:58 +0200 Subject: Introduce a Pcoq.Entry module for functions that ought to be exported. We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins. --- toplevel/coqloop.ml | 8 ++++---- toplevel/coqloop.mli | 2 +- toplevel/g_toplevel.mlg | 6 +++--- toplevel/vernac.ml | 6 +++--- 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d7ede1c2e..7ae15ac10 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf)); + ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -228,7 +228,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Pcoq.Gram.parsable (Stream.of_list []); + tokens = Pcoq.Parsable.make (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -253,7 +253,7 @@ let parse_to_dot = let rec discard_to_dot () = try - Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | Stm.End_of_input -> raise Stm.End_of_input diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 5c07a8bf3..b11f13d3c 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -18,7 +18,7 @@ type input_buffer = { mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 53d3eef23..5aba3d6b0 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -21,9 +21,9 @@ type vernac_toplevel = | VernacControl of vernac_control module Toplevel_ : sig - val vernac_toplevel : vernac_toplevel CAst.t Gram.entry + val vernac_toplevel : vernac_toplevel CAst.t Entry.t end = struct - let gec_vernac s = Gram.entry_create ("toplevel:" ^ s) + let gec_vernac s = Entry.create ("toplevel:" ^ s) let vernac_toplevel = gec_vernac "vernac_toplevel" end @@ -49,6 +49,6 @@ END { -let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa +let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa } diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c1bbb20d5..c914bbecf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -121,7 +121,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let in_echo = if echo then Some (open_utf8_file_in file) else None in let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in - let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in + let in_pa = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let rstate = ref state in (* For beautify, list of parsed sids *) let rids = ref [] in @@ -159,12 +159,12 @@ let load_vernac_core ~echo ~check ~interactive ~state file = rstate := state; done; input_cleanup (); - !rstate, !rids, Pcoq.Gram.comment_state in_pa + !rstate, !rids, Pcoq.Parsable.comment_state in_pa with any -> (* whatever the exception *) let (e, info) = CErrors.push any in input_cleanup (); match e with - | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa + | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa | reraise -> iraise (e, info) let process_expr ~state loc_ast = -- cgit v1.2.3