diff options
| -rw-r--r-- | toplevel/coqloop.ml | 33 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 25 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 50 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 23 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 11 |
5 files changed, 86 insertions, 56 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4641a2bc8..b608488c8 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -149,20 +149,6 @@ let valid_buffer_loc ib loc = not (Loc.is_ghost loc) && let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e -(* This is specific to the toplevel *) -let pr_loc loc = - if Loc.is_ghost loc then str"<unknown>" - else - let fname = loc.Loc.fname in - if CString.equal fname "" then - Loc.(str"Toplevel input, characters " ++ int loc.bp ++ - str"-" ++ int loc.ep ++ str":") - else - Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ - str", line " ++ int loc.line_nb ++ str", characters " ++ - int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ - str":") - (* Toplevel error explanation. *) let error_info_for_buffer ?loc buf = Option.map (fun loc -> @@ -177,7 +163,7 @@ let error_info_for_buffer ?loc buf = else (mt (), nloc) (* we are in batch mode, don't adjust location *) else (mt (), loc) - in pr_loc loc ++ hl + in Topfmt.pr_loc loc ++ hl ) loc (* Actual printing routine *) @@ -292,6 +278,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in | FileDependency (_,_) -> () | FileLoaded (_,_) -> () | Custom (_,_,_) -> () + (* Re-enable when we switch back to feedback-based error printing *) + | Message (Error,loc,msg) -> () + (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) | Message (lvl,loc,msg) -> TopErr.print_error_for_buffer ?loc lvl msg top_buffer @@ -318,11 +307,15 @@ let do_vernac sid = | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop else (Feedback.msg_error (str "There is no ML toplevel."); sid) - (* Exception printing is done now by the feedback listener. *) - (* XXX: We need this hack due to the side effects of the exception - printer and the reliance of Stm.define on attaching crutial - state to exceptions *) - | any -> ignore (CErrors.(iprint (push any))); sid + (* Exception printing should be done by the feedback listener, + however this is not yet ready so we rely on the exception for + now. *) + | any -> + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f5f43ff66..9cf075065 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -430,10 +430,10 @@ let get_native_name s = (** Prints info which is either an error or an anomaly and then exits with the appropriate error code *) -let fatal_error info anomaly = - let msg = info ++ fnl () in - Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; - exit (if anomaly then 129 else 1) +let fatal_error ?extra exn = + Topfmt.print_err_exn ?extra exn; + let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in + exit exit_code let parse_args arglist = let args = ref arglist in @@ -596,11 +596,7 @@ let parse_args arglist = in try parse () - with - | UserError(_, s) as e -> - if ismt s then exit 1 - else fatal_error (CErrors.print e) false - | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any) + with any -> fatal_error any let init_toplevel arglist = init_gc (); @@ -646,14 +642,13 @@ let init_toplevel arglist = check_vio_tasks (); outputstate () with any -> - let any = CErrors.push any in flush_all(); - let msg = - if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt () - else str "Error during initialization: " ++ CErrors.iprint any ++ fnl () + let extra = + if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) + then None + else Some (str "Error during initialization: ") in - let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in - fatal_error msg (is_anomaly (fst any)) + fatal_error ?extra any end; if !batch_mode then begin flush_all(); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f81f77e6e..8bcf2114b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -107,6 +107,16 @@ let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () with Proof_global.NoCurrentProof -> Pp.str "" +let vernac_error msg = + Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg; + flush_all (); + exit 1 + +(* Reenable when we get back to feedback printing *) +(* let is_end_of_input any = match any with *) +(* Stm.End_of_input -> true *) +(* | _ -> false *) + let rec interp_vernac sid po (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> @@ -161,17 +171,25 @@ and load_vernac verbosely sid file = * raised, which means that we raised the end of the file being loaded *) while true do let loc, ast = + Stm.parse_sentence !rsid in_pa + (* If an error in parsing occurs, we propagate the exception + so the caller of load_vernac will take care of it. However, + in the future it could be possible that we want to handle + all the errors as feedback events, thus in this case we + should relay the exception here for convenience. A + possibility is shown below, however we may want to refactor + this code: + try Stm.parse_sentence !rsid in_pa with - | Stm.End_of_input -> raise Stm.End_of_input - | any -> + | any when not is_end_of_input any -> let (e, info) = CErrors.push any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in Feedback.msg_error ?loc msg; iraise (e, info) + *) in - (* Printing of vernacs *) if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); Option.iter (vernac_echo loc) in_echo; @@ -231,13 +249,10 @@ let chop_extension f = let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in - if src <> tgt then begin - Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ - str "Source: " ++ str src ++ fnl () ++ - str "Target: " ++ str tgt); - flush_all (); - exit 1 - end + if src <> tgt then + vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt) let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt @@ -246,17 +261,15 @@ let ensure_vo v vo = ensure ".vo" v vo let ensure_vio v vio = ensure ".vio" v vio let ensure_exists f = - if not (Sys.file_exists f) then begin - Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f)); - exit 1 - end + if not (Sys.file_exists f) then + vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in - if not (List.is_empty pfs) then - (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in + if not (List.is_empty pfs) then vernac_error (str "There are pending proofs") + in match !Flags.compilation_mode with | BuildVo -> let long_f_dot_v = ensure_v f in @@ -311,5 +324,8 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - compile v f; + begin + try compile v f + with any -> Topfmt.print_err_exn any + end; CoqworkmgrApi.giveback 1 diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index c25dd55fb..a1835959c 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -260,6 +260,29 @@ let init_color_output () = *) let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning + +(* This is specific to the toplevel *) +let pr_loc loc = + if Loc.is_ghost loc then str"<unknown>" + else + let fname = loc.Loc.fname in + if CString.equal fname "" then + Loc.(str"Toplevel input, characters " ++ int loc.bp ++ + str"-" ++ int loc.ep ++ str":") + else + Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ + str", line " ++ int loc.line_nb ++ str", characters " ++ + int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ + str":") + +let print_err_exn ?extra any = + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg_loc = pr_loc (Option.default Loc.ghost loc) in + let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in + let msg = CErrors.iprint (e, info) ++ fnl () in + std_logger ~pre_hdr Feedback.Error msg + (* Output to file, used only in extraction so a candidate for removal *) let ft_logger old_logger ft ?loc level mesg = let id x = x in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 909dd7077..6c8e0ae2f 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -36,19 +36,22 @@ val get_depth_boxes : unit -> int option val set_margin : int option -> unit val get_margin : unit -> int option -(** Headers for tagging *) -val err_hdr : Pp.std_ppcmds -val ann_hdr : Pp.std_ppcmds - (** Console display of feedback, we may add some location information *) val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit +(** Color output *) val init_color_output : unit -> unit val clear_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +(** Error printing *) +(* To be deprecated when we can fully move to feedback-based error + printing. *) +val pr_loc : Loc.t -> Pp.std_ppcmds +val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit + (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b |