From 3a7d9fcafedc4987d0748a8717b2b012a779de39 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Feb 2017 14:14:34 +0100
Subject: [stm] Remove edit_id.

We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.

Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.

XML protocol clients are unaffected, they rely on the instead on the
Fail value.

This commit supersedes PR#203.
---
 lib/feedback.ml  | 10 ++++------
 lib/feedback.mli | 23 +++++++++--------------
 2 files changed, 13 insertions(+), 20 deletions(-)

(limited to 'lib')

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}
 
-- 
cgit v1.2.3


From ce2b2058587224ade9261cd4127ef4f6e94d356b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 27 Feb 2017 20:16:40 +0100
Subject: [stm] Port the toplevel to the STM.

- We clean-up `Vernac` and make it use the STM API.

- Now functions in `Vernac` for use in the toplevel and compiler take
  an starting `Stateid.t`.

- Duplicated `Stm.interp` entry point is removed.

- The XML protocol call `interp` is disabled.
---
 lib/flags.ml  | 2 --
 lib/flags.mli | 3 +--
 2 files changed, 1 insertion(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 5b080151cd..ef5eddfb29 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
diff --git a/lib/flags.mli b/lib/flags.mli
index bd365e6538..f5e1c96f9a 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -46,9 +46,8 @@ val in_toplevel : bool ref
 
 val profile : bool
 
+(* Legacy flags *)
 val print_emacs : bool ref
-val coqtop_ui : bool ref
-
 val xml_export : bool ref
 
 val ide_slave : bool ref
-- 
cgit v1.2.3


From 55bddb4bf35fa68318aa57a5fa8a113d1fe51159 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Feb 2017 02:31:16 +0100
Subject: [flags] Documentation and a minor tweak.

Mostly documentation and making a couple of local flags, local.
---
 lib/flags.ml  |  7 -------
 lib/flags.mli | 23 ++++++++++++++++++-----
 2 files changed, 18 insertions(+), 12 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index ef5eddfb29..d87d9e7295 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -95,7 +95,6 @@ let time = ref false
 
 let raw_print = ref false
 
-let record_print = ref true
 
 let univ_print = ref false
 
@@ -181,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 f5e1c96f9a..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
@@ -47,18 +52,26 @@ val in_toplevel : bool ref
 val profile : bool
 
 (* 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
@@ -68,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
@@ -79,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
 
@@ -110,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 *)
-- 
cgit v1.2.3