(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(* Quickfix management *)
type t = Loc.t * Pp.t let make ~loc txt = loc, txt let pp (_,x) = x let pp_wloc (loc,x) = letopen Pp in
h (str "Replace " ++ Loc.pr loc ++ str " with " ++ x) let loc (l,_) = l
let handle_stack = ref []
let register h = handle_stack := h::!handle_stack
let rec accumulate_qf acc stk e = match stk with
| [] -> acc
| h::stk -> accumulate_qf (h e :: acc) stk e
let from_exception e = try
Ok (CList.flatten (accumulate_qf [] !handle_stack e)) with exn -> let ei = Exninfo.capture exn in
Error ei
letprint e = letopen Pp in match e with
| [] -> mt ()
| qf -> letopen Pp in let qf = prlist_with_sep cut pp_wloc qf in
v 0 (prlist_with_sep cut (fun x -> x) [str "Quickfix:"; qf])
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.2Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.