diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqloop.mli | 2 | ||||
| -rw-r--r-- | toplevel/g_toplevel.mlg | 6 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 |
4 files changed, 11 insertions, 11 deletions
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 = |