| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/lib/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 3 kB |
|
Quelle feedback.mli Sprache: SML |
|||||||||
|
(************************************************************************)
(* * 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) *) (************************************************************************) open Xml_datatype (* Legacy-style logging messages (used to be in Pp) *) type level = | Debug | Info | Notice | Warning | Error (** Document unique identifier for serialization *) type doc_id = int (** Rocq "semantic" infos obtained during execution *) type route_id = int val default_route : route_id type feedback_content = (* STM mandatory data (must be displayed) *) | Processed | Incomplete | Complete (* STM optional data *) | ProcessingIn of string | InProgress of int | WorkerStatus of string * string (* Generally useful metadata *) | AddedAxiom | GlobRef of Loc.t * string * string * string * string | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string (* Extra metadata *) | Custom of Loc.t option * string * xml (* Generic messages *) | Message of level * Loc.t option * Quickfix.t list * Pp.t type feedback = { doc_id : doc_id; (* The document being concerned *) span_id : Stateid.t; (* The document part concerned *) route : route_id; (* Extra routing info *) contents : feedback_content; (* The payload *) } (** {6 Feedback sent, even asynchronously, to the user interface} *) (* The interpreter assigns a state_id to the ast, and feedbacks happening * during interpretation are attached to it. *) (** [add_feeder f] adds a feeder listiner [f], returning its id *) val add_feeder : (feedback -> unit) -> int (** [del_feeder fid] removes the feeder with id [fid] *) val del_feeder : int -> unit (** [feedback ?did ?sid ?route fb] produces feedback [fb], with [route] and [did, sid] set appropiatedly, if absent, it will use the defaults set by [set_id_for_feedback] *) val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit (** [set_id_for_feedback route id] Set the defaults for feedback *) val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit (** {6 output functions} *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) val msg_info : ?loc:Loc.t -> Pp.t -> unit (** Message that displays information, usually in verbose mode, such as [Foobar is defined] *) val msg_notice : ?loc:Loc.t -> Pp.t -> unit (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) val msg_warning : ?loc:Loc.t -> ?quickfix:Quickfix.t list -> Pp.t -> unit (** Message indicating that something went wrong, but without serious consequences. A list of quick fixes, in the VSCode sense, can be provided *) val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) val console_feedback_listener : Format.formatter -> feedback -> unit (** Helper for tools willing to print to the feedback system *) val warn_no_listeners : bool ref (** The library will print a warning to the console if no listener is available by default; ML-clients willing to use Rocq without a feedback handler should set this to false. *) ¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28