Merge PR#441: Port Toplevel to the Stm API

4 files changed, 32 insertions, 36 deletions

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 7d9d6bf7f0..df6fe3a629 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 4bbdfcb5b6..bdd236ac78 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 5b080151cd..d87d9e7295 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
 
@@ -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 bd365e6538..c5c4a15aaa 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,9 +81,12 @@ 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
 
+(* Silent/verbose, both actually controlled by a single flag so they
+   are mutually exclusive *)
 val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
@@ -80,6 +95,7 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
+(* Miscellaneus flags for vernac *)
 val make_auto_intros : bool -> unit
 val is_auto_intros : unit -> bool
 
@@ -111,10 +127,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 *)