diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/feedback.ml | 10 | ||||
| -rw-r--r-- | lib/feedback.mli | 23 | ||||
| -rw-r--r-- | lib/flags.ml | 25 | ||||
| -rw-r--r-- | lib/flags.mli | 38 |
4 files changed, 49 insertions, 47 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index 7d9d6bf7f..df6fe3a62 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -15,9 +15,6 @@ type level = | Warning | Error -type edit_id = int -type state_id = Stateid.t -type edit_or_state_id = Edit of edit_id | State of state_id type route_id = int type feedback_content = @@ -38,9 +35,9 @@ type feedback_content = | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { - id : edit_or_state_id; + id : Stateid.t; + route : route_id; contents : feedback_content; - route : route_id; } let default_route = 0 @@ -56,7 +53,8 @@ let add_feeder = let del_feeder fid = Hashtbl.remove feeders fid -let feedback_id = ref (Edit 0) +let default_route = 0 +let feedback_id = ref Stateid.dummy let feedback_route = ref default_route let set_id_for_feedback ?(route=default_route) i = diff --git a/lib/feedback.mli b/lib/feedback.mli index 4bbdfcb5b..bdd236ac7 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -16,11 +16,8 @@ type level = | Warning | Error -(** Coq "semantic" infos obtained during parsing/execution *) -type edit_id = int -type state_id = Stateid.t -type edit_or_state_id = Edit of edit_id | State of state_id +(** Coq "semantic" infos obtained during execution *) type route_id = int val default_route : route_id @@ -46,17 +43,16 @@ type feedback_content = | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { - id : edit_or_state_id; (* The document part concerned *) - contents : feedback_content; (* The payload *) + 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} *) -(* Morally the parser gets a string and an edit_id, and gives back an AST. - * Feedbacks during the parsing phase are attached to this edit_id. - * The interpreter assignes an exec_id to the ast, and feedbacks happening - * during interpretation are attached to the exec_id. - * Only one among state_id and edit_id can be provided. *) + +(* The interpreter assignes an 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 @@ -67,11 +63,10 @@ val del_feeder : int -> unit (** [feedback ?id ?route fb] produces feedback fb, with [route] and [id] set appropiatedly, if absent, it will use the defaults set by [set_id_for_feedback] *) -val feedback : - ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit +val feedback : ?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 -> edit_or_state_id -> unit +val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit (** {6 output functions} diff --git a/lib/flags.ml b/lib/flags.ml index 5b080151c..00f515b5a 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -86,8 +86,6 @@ let in_toplevel = ref false let profile = false let print_emacs = ref false -let coqtop_ui = ref false - let xml_export = ref false let ide_slave = ref false @@ -97,7 +95,6 @@ let time = ref false let raw_print = ref false -let record_print = ref true let univ_print = ref false @@ -146,16 +143,16 @@ let beautify = ref false let beautify_file = ref false (* Silent / Verbose *) -let silent = ref false -let make_silent flag = silent := flag; () -let is_silent () = !silent -let is_verbose () = not !silent +let quiet = ref false +let silently f x = with_option quiet f x +let verbosely f x = without_option quiet f x -let silently f x = with_option silent f x -let verbosely f x = without_option silent f x +let if_silent f x = if !quiet then f x +let if_verbose f x = if not !quiet then f x -let if_silent f x = if !silent then f x -let if_verbose f x = if not !silent then f x +let make_silent flag = quiet := flag +let is_silent () = !quiet +let is_verbose () = not !quiet let auto_intros = ref true let make_auto_intros flag = auto_intros := flag @@ -183,12 +180,6 @@ let warn = ref true let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x -(* The number of printed hypothesis in a goal *) - -let print_hyps_limit = ref (None : int option) -let set_print_hyps_limit n = print_hyps_limit := n -let print_hyps_limit () = !print_hyps_limit - (* Flags for external tools *) let browser_cmd_fmt = diff --git a/lib/flags.mli b/lib/flags.mli index bd365e653..0b00ac13c 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -8,6 +8,8 @@ (** Global options of the system. *) +(** Command-line flags *) + val boot : bool ref val load_init : bool ref @@ -16,8 +18,11 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref val compilation_output_name : string option ref +(* Flag set when the test-suite is called. Its only effect to display + verbose information for `Fail` *) val test_mode : bool ref +(** Async-related flags *) type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref type cache = Force @@ -46,20 +51,27 @@ val in_toplevel : bool ref val profile : bool -val print_emacs : bool ref -val coqtop_ui : bool ref +(* Legacy flags *) +(* -emacs option: printing includes emacs tags, will affect stm caching. *) +val print_emacs : bool ref +(* -xml option: xml hooks will be called *) val xml_export : bool ref +(* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref val ideslave_coqtop_flags : string option ref +(* -time option: every command will be wrapped with `Time` *) val time : bool ref +(* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref +(* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -val record_print : bool ref + +(* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current @@ -69,17 +81,27 @@ val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string +(* Beautify command line flags, should move to printing? *) val beautify : bool ref val beautify_file : bool ref -val make_silent : bool -> unit -val is_silent : unit -> bool -val is_verbose : unit -> bool +(* Coq quiet mode. Note that normal mode is called "verbose" here, + whereas [quiet] supresses normal output such as goals in coqtop *) +val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +(* Deprecated *) +val make_silent : bool -> unit +[@@ocaml.deprecated "Please use Flags.quiet"] +val is_silent : unit -> bool +[@@ocaml.deprecated "Please use Flags.quiet"] +val is_verbose : unit -> bool +[@@ocaml.deprecated "Please use Flags.quiet"] + +(* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool @@ -111,10 +133,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b (** Temporarily extends the reference to a list *) val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b -(** If [None], no limit *) -val set_print_hyps_limit : int option -> unit -val print_hyps_limit : unit -> int option - (** Options for external tools *) (** Returns string format for default browser to use from Coq or CoqIDE *) |