From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/coqloop.ml | 116 +++++++++++++++++++++++++--------------------------- 1 file changed, 55 insertions(+), 61 deletions(-) (limited to 'toplevel/coqloop.ml') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 063ed896..e9771cfa 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -7,12 +7,14 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Flags open Vernac open Pcoq +let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x + (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -21,7 +23,7 @@ type input_buffer = { mutable str : string; (* 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 : Gram.parsable; (* stream of tokens *) + mutable tokens : Gram.coq_parsable; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -32,7 +34,7 @@ let resize_buffer ibuf = ibuf.str <- nstr (* Delete all irrelevant lines of the input buffer. Keep the last line - in the buffer (useful when there are several commands on the same line. *) + in the buffer (useful when there are several commands on the same line). *) let resynch_buffer ibuf = match ibuf.bols with @@ -59,7 +61,7 @@ let prompt_char ic ibuf count = | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !print_emacs then msgerr (str (ibuf.prompt())); + if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; @@ -144,44 +146,23 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in - let loc = Loc.make_loc (bp,ep) in - (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ - highlight_lines ++ fnl ()) + let loc = Loc.make_loc (bp,ep) in + (Pp.pr_loc loc ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) -let print_location_in_file {outer=s;inner=fname} loc = - let errstrm = str"Error while reading " ++ str s in +let print_location_in_file loc = + let fname = loc.Loc.fname in + let errstrm = str"Error while reading " ++ str fname in if Loc.is_ghost loc then hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl () else - let errstrm = - if String.equal s fname then mt() else errstrm ++ str":" ++ fnl() + let errstrm = mt () + (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *) in - let (bp,ep) = Loc.unloc loc in - let line_of_pos lin bol cnt = - try - let ic = open_in fname in - let rec line_of_pos lin bol cnt = - if cnt < bp then - if input_char ic == '\n' - then line_of_pos (lin + 1) (cnt +1) (cnt+1) - else line_of_pos lin bol (cnt+1) - else (lin, bol) - in - let rc = line_of_pos lin bol cnt in - close_in ic; - rc - with Sys_error _ -> 0, 0 in - try - let (line, bol) = line_of_pos 1 0 0 in - hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++ - str", line " ++ int line ++ str", characters " ++ - Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++ - fnl () - with e when Errors.noncritical e -> - hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl () + let open Loc in + hov 0 (* No line break so as to follow emacs error message format *) + (errstrm ++ Pp.pr_loc loc) let valid_buffer_loc ib loc = not (Loc.is_ghost loc) && @@ -262,14 +243,15 @@ let locate_exn = function let print_toplevel_error (e, info) = let loc = Option.default Loc.ghost (Loc.get_loc info) in - let locmsg = match Vernac.get_exn_files info with - | Some files -> print_location_in_file files loc - | None -> + let fname = loc.Loc.fname in + let locmsg = + if Loc.is_ghost loc || String.equal fname "" then if locate_exn e && valid_buffer_loc top_buffer loc then - print_highlight_location top_buffer loc + print_highlight_location top_buffer loc else mt () + else print_location_in_file loc in - locmsg ++ Errors.iprint (e, info) + locmsg ++ CErrors.iprint (e, info) (* Read the input stream until a dot is encountered *) let parse_to_dot = @@ -288,14 +270,16 @@ let rec discard_to_dot () = try Gram.entry_parse parse_to_dot top_buffer.tokens with - | Compat.Token.Error _ | Lexer.Error.E _ -> discard_to_dot () + | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | End_of_input -> raise End_of_input - | e when Errors.noncritical e -> () + | e when CErrors.noncritical e -> () -let read_sentence () = - try Vernac.parse_sentence (top_buffer.tokens, None) +let read_sentence input = + try + let (loc, _ as r) = Vernac.parse_sentence input in + CWarnings.set_current_loc loc; r with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in discard_to_dot (); iraise reraise @@ -310,23 +294,23 @@ let read_sentence () = *) let do_vernac () = - msgerrnl (mt ()); - if !print_emacs then msgerr (str (top_buffer.prompt())); + top_stderr (fnl()); + if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try - Vernac.eval_expr (read_sentence ()) + let input = (top_buffer.tokens, None) in + Vernac.process_expr top_buffer.tokens (read_sentence input) with - | End_of_input | Errors.Quit -> - msgerrnl (mt ()); pp_flush(); raise Errors.Quit - | Errors.Drop -> (* Last chance *) - if Mltop.is_ocaml_top() then raise Errors.Drop - else ppnl (str"Error: There is no ML toplevel." ++ fnl ()) + | End_of_input | CErrors.Quit -> + top_stderr (fnl ()); raise CErrors.Quit + | CErrors.Drop -> (* Last chance *) + if Mltop.is_ocaml_top() then raise CErrors.Drop + else Feedback.msg_error (str"There is no ML toplevel.") | any -> - let any = Errors.push any in - Format.set_formatter_out_channel stdout; + let any = CErrors.push any in let msg = print_toplevel_error any ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; - pp_flush () + Format.pp_print_flush !Pp_control.std_ft () (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -343,18 +327,28 @@ let feed_emacs = function | _ -> () *) +(* Flush in a compatible order with 8.5 *) +(* This mimics the semantics of the old Pp.flush_all *) +let loop_flush_all () = + Pervasives.flush stderr; + Pervasives.flush stdout; + Format.pp_print_flush !Pp_control.std_ft (); + Format.pp_print_flush !Pp_control.err_ft () + let rec loop () = Sys.catch_break true; if !Flags.print_emacs then Vernacentries.qed_display_script := false; Flags.coqtop_ui := true; try reset_input_buffer stdin top_buffer; - while true do do_vernac(); flush_all() done + while true do do_vernac(); loop_flush_all () done with - | Errors.Drop -> () - | Errors.Quit -> exit 0 + | CErrors.Drop -> () + | CErrors.Quit -> exit 0 | any -> - msgerrnl (str"Anomaly: main loop exited with exception: " ++ + Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ - fnl() ++ str"Please report."); + fnl() ++ + str"Please report" ++ + strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); loop () -- cgit v1.2.3