From bd458575ba7f767e3b939fad5d628a9cb24e6bb2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 18:23:41 +0100 Subject: [pp] Add anomaly header to anomaly error messages. This patch restores the proper printing of anomalies in coqtop / coqc / coqide. Currently, they are printed with an `Error` header, whereas they should be printed with an `Anomaly" header. This reopens an unfinished debate started in #390 , about how to properly do "message" headers. Prior to #390, headers were handled inconsistently, sometimes, `Error` or `Anomaly` were added in `CErrors`, which lives below of the tagging system, thus some times we got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789), but some other times the headers were added by the message handlers in Feedback. PR #390 takes the position of identifying the messages with the `Feedback.level` tag, and letting the backends to the tagging. This makes sense as the backends may want to interpret the "headers" in any way they'd like. For instance, instead of printing: `Error: foo` they may want to insert an image. Note that this implies that CoqIDE doesn't currently insert an error header on the first error case. This could be easily solved, but for anomalies we could do in any of the ways explained below. There are thus two natural ways to handle anomalies here: One is to tag them as errors, but add a text header, this is done now, with the small optimization in the case the handled has access to the exception itself. The second way is to add a new `Feedback.level` category and tag the anomalies appropriately. We would need also to modify Fail in this case, or to completely remove it from the protocol. I guess feedback from the rest of developers is needed before committing to a strategy, for now this patch should be good. --- vernac/topfmt.ml | 1 + vernac/topfmt.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'vernac') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index f843484f7..e3c0a1709 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -136,6 +136,7 @@ let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc () let info_hdr = mt () let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () let err_hdr = tag Tag.error (str "Error:") ++ spc () +let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () let make_body quoter info ?loc s = let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 1555f80a9..0e122f46e 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -38,6 +38,7 @@ 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 *) val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit -- cgit v1.2.3 From 8cfe40dbc02156228a529c01190c50d825495013 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 22 Mar 2017 19:06:54 +0100 Subject: Ensuring static invariants about handling of pending evars in Pretyping. All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. --- engine/evd.ml | 4 ---- engine/evd.mli | 4 ---- plugins/ltac/tacinterp.ml | 2 +- pretyping/pretyping.ml | 10 +++++----- pretyping/pretyping.mli | 4 ++-- pretyping/unification.ml | 4 ++-- pretyping/unification.mli | 4 ++-- tactics/tactics.ml | 16 ++++++---------- tactics/tactics.mli | 2 +- vernac/command.ml | 8 ++++---- vernac/lemmas.ml | 2 +- vernac/record.ml | 2 +- 12 files changed, 25 insertions(+), 37 deletions(-) (limited to 'vernac') diff --git a/engine/evd.ml b/engine/evd.ml index 62d396395..b7d56a698 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1157,10 +1157,6 @@ let set_extra_data extras evd = { evd with extras } (*******************************************************************) -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - type open_constr = evar_map * constr (*******************************************************************) diff --git a/engine/evd.mli b/engine/evd.mli index 993ed300b..5619b7af2 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -601,10 +601,6 @@ val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - type open_constr = evar_map * constr (* Special case when before is empty *) (** Partially constructed constrs. *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 155cb31d8..6ed96c1fb 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1787,7 +1787,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) - ((sigma,sigma'),c) clp eqpat) sigma') + (sigma,c) clp eqpat) sigma') end } (* Derived basic tactics *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f92110ea5..2e215b605 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -333,8 +333,8 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let solve_remaining_evars flags env current_sigma init_sigma = + let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then @@ -343,12 +343,12 @@ let solve_remaining_evars flags env current_sigma pending = if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; !evdref -let check_evars_are_solved env current_sigma pending = - let frozen,pending = frozen_and_pending_holes pending in +let check_evars_are_solved env current_sigma init_sigma = + let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = - let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in + let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2c6aa7a21..23957d557 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -129,13 +129,13 @@ val type_uconstr : [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : inference_flags -> - env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map + env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, reporting an appropriate error message *) val check_evars_are_solved : - env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit + env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a91c30df6..11771f7ba 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1520,7 +1520,7 @@ let default_matching_merge_flags sigma = use_pattern_unification = true; } -let default_matching_flags (sigma,_) = +let default_matching_flags sigma = let flags = default_matching_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = default_matching_merge_flags sigma; @@ -1658,7 +1658,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * (evar_map * constr) * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool type 'r abstraction_result = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ad882a9f..c63502eae 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -71,11 +71,11 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma + env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma type 'r abstraction_result = Names.Id.t * named_context_val * diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 84d09d833..1e8082f88 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1154,10 +1154,9 @@ let tactic_infer_flags with_evar = { let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> let (cbl, sigma') = run_delayed env sigma f in - let pending = (sigma,sigma') in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma') - (tac clear_flag (pending,cbl)) + (tac clear_flag (sigma,cbl)) | clear_flag,ElimOnAnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) @@ -1165,8 +1164,7 @@ let onOpenInductionArg env sigma tac = function (fun c -> Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in - let pending = (sigma,sigma) in - tac clear_flag (pending,(c,NoBindings)) + tac clear_flag (sigma,(c,NoBindings)) end })) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) @@ -1174,8 +1172,7 @@ let onOpenInductionArg env sigma tac = function (try_intros_until_id_check id) (Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in - let pending = (sigma,sigma) in - tac clear_flag (pending,(mkVar id,NoBindings)) + tac clear_flag (sigma,(mkVar id,NoBindings)) end }) let onInductionArg tac = function @@ -1198,10 +1195,9 @@ let map_destruction_arg f sigma = function let finish_delayed_evar_resolution with_evars env sigma f = let ((c, lbind), sigma') = run_delayed env sigma f in - let pending = (sigma,sigma') in let sigma' = Sigma.Unsafe.of_evar_map sigma' in let flags = tactic_infer_flags with_evars in - let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in + let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in (Sigma.to_evar_map sigma', (c, lbind)) let with_no_bindings (c, lbind) = @@ -4525,11 +4521,11 @@ let induction_destruct isrec with_evars (lc,elim) = let induction ev clr c l e = induction_gen clr true ev e - (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None + ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = induction_gen clr false ev e - (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None + ((Evd.empty,(c,NoBindings)),(None,l)) None (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7acfb6286..354ac50b4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -385,7 +385,7 @@ val letin_tac : (bool * intro_pattern_naming) option -> (** Common entry point for user-level "set", "pose" and "remember" *) val letin_pat_tac : (bool * intro_pattern_naming) option -> - Name.t -> pending_constr -> clause -> unit Proofview.tactic + Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic (** {6 Generalize tactics. } *) diff --git a/vernac/command.ml b/vernac/command.ml index 4b4f4d271..849596f07 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -139,7 +139,7 @@ let interp_definition pl bl p red_option c ctypopt = red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps let check_definition (ce, evd, _, imps) = - check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); + check_evars_are_solved (Global.env ()) evd Evd.empty; ce let warn_local_declaration = @@ -299,7 +299,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in - let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in let ctx = Evd.universe_context_set evd in @@ -604,7 +604,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = () in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in + let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in evdref := sigma; (* Compute renewed arities *) let nf,_ = e_nf_evars_and_universes evdref in @@ -1142,7 +1142,7 @@ let interp_recursive isfix fixl notations = (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd (Evd.empty,evd); + check_evars_are_solved env evd Evd.empty; if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env isfix (List.combine fixnames fixdefs) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 798a238c7..409676276 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -463,7 +463,7 @@ let start_proof_com ?inference_hook kind thms hook = let t', imps' = interp_type_evars_impls ~impls env evdref t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars flags env !evdref Evd.empty; let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/vernac/record.ml b/vernac/record.ml index b494430c2..07cfd9ebb 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -141,7 +141,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in let sigma = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in let evars, nf = Evarutil.nf_evars_and_universes sigma in let arity = nf t' in let arity, evars = -- cgit v1.2.3 From 63cfc77ddf3586262d905dc351b58669d185a55e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 31 Mar 2017 20:38:52 +0200 Subject: [toplevel] Remove exception error printer in favor of feedback printer. We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429 --- lib/pp.ml | 19 ----- lib/pp.mli | 1 - test-suite/output/ErrorInModule.out | 1 + test-suite/output/ErrorInSection.out | 1 + test-suite/output/qualification.out | 1 + toplevel/coqloop.ml | 134 ++++++++++++++++------------------- toplevel/coqloop.mli | 7 +- toplevel/coqtop.ml | 4 +- vernac/topfmt.ml | 24 +++---- vernac/topfmt.mli | 7 +- 10 files changed, 81 insertions(+), 118 deletions(-) (limited to 'vernac') diff --git a/lib/pp.ml b/lib/pp.ml index 9f33756df..66feae761 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -116,25 +116,6 @@ let strbrk s = else if p = n then [] else [str (String.sub s p (n-p))] in Ppcmd_glue (aux 0 0) -let pr_loc_pos loc = - if Loc.is_ghost loc then (str"") - else - let loc = Loc.unloc loc in - int (fst loc) ++ str"-" ++ int (snd loc) - -let pr_loc loc = - if Loc.is_ghost loc then str"" ++ fnl () - 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":" ++ fnl ()) - 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":" ++ fnl()) - let ismt = function | Ppcmd_empty -> true | _ -> false (* boxing commands *) diff --git a/lib/pp.mli b/lib/pp.mli index 802ffe8e7..7a191b01a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -171,7 +171,6 @@ val surround : std_ppcmds -> std_ppcmds (** Surround with parenthesis. *) val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds -val pr_loc : Loc.t -> std_ppcmds (** {6 Main renderers, to formatter and to string } *) diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out index 851ecd930..776dfeb55 100644 --- a/test-suite/output/ErrorInModule.out +++ b/test-suite/output/ErrorInModule.out @@ -1,2 +1,3 @@ File "stdin", line 3, characters 20-31: Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out index 851ecd930..776dfeb55 100644 --- a/test-suite/output/ErrorInSection.out +++ b/test-suite/output/ErrorInSection.out @@ -1,2 +1,3 @@ File "stdin", line 3, characters 20-31: Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out index 9300c3f54..e9c70d1ef 100644 --- a/test-suite/output/qualification.out +++ b/test-suite/output/qualification.out @@ -1,3 +1,4 @@ File "stdin", line 19, characters 0-7: Error: Signature components for label test do not match: expected type "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". + diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index bbe4fb84c..8e6f9ffb5 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -52,7 +52,6 @@ let resynch_buffer ibuf = to avoid interfering with utf8. Compatibility code removed. *) let emacs_prompt_startstring() = Printer.emacs_str "" - let emacs_prompt_endstring() = Printer.emacs_str "" (* Read a char in an input channel, displaying a prompt at every @@ -83,6 +82,7 @@ let reset_input_buffer ic ibuf = ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) +module TopErr = struct (* Given a location, returns the list of locations of each line. The last line is returned separately. It also checks the location bounds. *) @@ -124,10 +124,11 @@ let blanch_utf8_string s bp ep = let open Bytes in done; Bytes.sub_string s' 0 !j +let adjust_loc_buf ib loc = let open Loc in + { loc with ep = loc.ep - ib.start; bp = loc.bp - ib.start } + let print_highlight_location ib loc = let (bp,ep) = Loc.unloc loc in - let bp = bp - ib.start - and ep = ep - ib.start in let highlight_lines = match get_bols_of_loc ib (bp,ep) with | ([],(bl,el)) -> @@ -147,28 +148,58 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in - 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 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 = mt () - (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *) - in - let open Loc in - hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ Pp.pr_loc loc) + highlight_lines 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"" + 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 -> + let fname = loc.Loc.fname in + let hl, loc = + (* We are in the toplevel *) + if String.equal fname "" then + let nloc = adjust_loc_buf buf loc in + if valid_buffer_loc buf loc then + (fnl () ++ print_highlight_location buf nloc, nloc) + (* in the toplevel, but not a valid buffer *) + else (mt (), nloc) + (* we are in batch mode, don't adjust location *) + else (mt (), loc) + in pr_loc loc ++ hl + ) loc + +(* Actual printing routine *) +let print_error_for_buffer ?loc lvl msg buf = + let pre_hdr = error_info_for_buffer ?loc buf in + if !Flags.print_emacs + then Topfmt.emacs_logger ?pre_hdr lvl msg + else Topfmt.std_logger ?pre_hdr lvl msg + +let print_toplevel_parse_error (e, info) buf = + let loc = Loc.get_loc info in + let lvl = Feedback.Error in + let msg = CErrors.iprint (e, info) in + print_error_for_buffer ?loc lvl msg buf + +end + (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing from cycling. *) @@ -178,18 +209,6 @@ let make_prompt () = with Proof_global.NoCurrentProof -> "Coq < " -(*let build_pending_list l = - let pl = ref ">" in - let l' = ref l in - let res = - while List.length !l' > 1 do - pl := !pl ^ "|" Names.Id.to_string x; - l':=List.tl !l' - done in - let last = try List.hd !l' with _ -> in - "<"^l' -*) - (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global backtracking) and the current proof state [p] (for proof @@ -234,29 +253,6 @@ let set_prompt prompt = ^ prompt () ^ emacs_prompt_endstring()) -(* The following exceptions need not be located. *) - -let locate_exn = function - | Out_of_memory | Stack_overflow | Sys.Break -> false - | _ -> true - -(* Toplevel error explanation. *) - -let print_toplevel_error (e, info) = - let loc = Option.default Loc.ghost (Loc.get_loc info) in - 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 - else mt () - else print_location_in_file loc - in - let hdr_text = - if CErrors.is_anomaly e then Topfmt.ann_hdr else Topfmt.err_hdr in - let hdr msg = hov 0 (hdr_text ++ msg) in - locmsg ++ hdr (CErrors.iprint (e, info)) - (* Read the input stream until a dot is encountered *) let parse_to_dot = let rec dot st = match Compat.get_tok (Stream.next st) with @@ -285,6 +281,7 @@ let read_sentence input = with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); + TopErr.print_toplevel_parse_error reraise top_buffer; iraise reraise (** Coqloop Console feedback handler *) @@ -302,17 +299,8 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in | FileDependency (_,_) -> () | FileLoaded (_,_) -> () | Custom (_,_,_) -> () - | Message (Error,loc,msg) -> - (* We ignore errors here as we (still) have a different error - printer for the toplevel. It is hard to solve due the many - error paths presents, and the different compromise of feedback - error forwaring in the stm depending on the mode *) - () | Message (lvl,loc,msg) -> - if !Flags.print_emacs then - Topfmt.emacs_logger ?loc lvl msg - else - Topfmt.std_logger ?loc lvl msg + TopErr.print_error_for_buffer ?loc lvl msg top_buffer (** [do_vernac] reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: @@ -336,13 +324,13 @@ let do_vernac () = top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else top_stderr (str "There is no ML toplevel.") - | any -> - (** Main error printer, note that this didn't it the "emacs" - legacy path. *) - let any = CErrors.push any in - let msg = print_toplevel_error any ++ fnl () in - top_stderr msg + else Feedback.msg_error (str "There is no ML toplevel.") + (* 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))) + (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -369,7 +357,7 @@ let rec loop () = | CErrors.Drop -> () | CErrors.Quit -> exit 0 | any -> - top_stderr (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" ++ diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index eb61084e0..8a34ded6d 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -26,12 +26,7 @@ type input_buffer = { val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit -(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D - May raise only the following exceptions: [Drop] and [End_of_input], - meaning we get out of the Coq loop. *) - -val print_toplevel_error : Exninfo.iexn -> std_ppcmds - +(** Toplevel feedback printer. *) val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0cd5498fe..4968804fd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -653,10 +653,10 @@ let init_toplevel arglist = flush_all(); let msg = if !batch_mode then mt () - else str "Error during initialization:" ++ fnl () + else str "Error during initialization: " ++ CErrors.iprint any ++ fnl () in let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in - fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any)) + fatal_error msg (is_anomaly (fst any)) end; if !batch_mode then begin flush_all(); diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e3c0a1709..ee5536692 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -108,7 +108,7 @@ end type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with fmt strm = +let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () @@ -138,19 +138,17 @@ let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () let err_hdr = tag Tag.error (str "Error:") ++ spc () let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () -let make_body quoter info ?loc s = - let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in - quoter (hov 0 (loc ++ info ++ s)) +let make_body quoter info ?pre_hdr s = + pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s)) (* Generic logger *) -let gen_logger dbg err ?loc level msg = match level with - | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?loc msg) - | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?loc msg) - (* XXX: What to do with loc here? *) - | Notice -> msgnl_with !std_ft msg +let gen_logger dbg err ?pre_hdr level msg = match level with + | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) + | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) + | Notice -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_hdr ?loc msg)) () - | Error -> msgnl_with !err_ft (make_body err err_hdr ?loc msg) + msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) () + | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg) (** Standard loggers *) @@ -159,8 +157,8 @@ let gen_logger dbg err ?loc level msg = match level with *) let std_logger_cleanup = ref (fun () -> ()) -let std_logger ?loc level msg = - gen_logger (fun x -> x) (fun x -> x) ?loc level msg; +let std_logger ?pre_hdr level msg = + gen_logger (fun x -> x) (fun x -> x) ?pre_hdr level msg; !std_logger_cleanup () (** Color logging. Moved from Ppstyle, it may need some more refactoring *) diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0e122f46e..909dd7077 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -40,10 +40,9 @@ val get_margin : unit -> int option val err_hdr : Pp.std_ppcmds val ann_hdr : Pp.std_ppcmds -(** Console display of feedback *) -val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit - -val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit +(** 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 val init_color_output : unit -> unit val clear_styles : unit -> unit -- cgit v1.2.3