[stm] Improve error messages on add/parse.

As suggested by @psteckler in #524 , we give more explicit information
about what is wrong.

We also provide some debug information for the possible dangerous case
of having the tip go out of sync with the real installed state (which
will make parsing fail if there was some changes to the parser).

We also fix a couple of typos noticed by Paul, thanks Paul.

2 files changed, 18 insertions, 4 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7e7bb98580..fe0b587b11 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -148,7 +148,7 @@ document type". This allows for a more uniform handling of printing
 
 - The main parsing entry point has also been moved to the
   `Stm`. Parsing is considered a synchronous operation so it will
-  either succeed of emit an exception.
+  either succeed or raise an exception.
 
 - `Feedback` is now only emitted for asynchronous operations. As a
   consequence, it always carries a valid stateid and the type has
@@ -167,7 +167,7 @@ document type". This allows for a more uniform handling of printing
 
 ** XML Protocol **
 
-- The legacy `interp` call has been turned into a noop.
+- The legacy `Interp` call has been turned into a noop.
 
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
diff --git a/stm/stm.ml b/stm/stm.ml
index 8d212a6a08..d11aea6c41 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -699,6 +699,9 @@ module State : sig
   val proof_part_of_frozen : frozen_state -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
+  (* Only for internal use to catch problems in parse_sentence, should
+     be removed in the state handling refactoring.  *)
+  val cur_id : Stateid.t ref
 end = struct (* {{{ *)
 
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
@@ -2669,9 +2672,19 @@ let parse_sentence sid pa =
      proper state makes the error resilience code fail *)
   (* Reach.known_state ~cache:`Yes sid; *)
   let cur_tip = VCS.cur_tip () in
+  let real_tip = !State.cur_id in
   if not (Stateid.equal sid cur_tip) then
     user_err ~hdr:"Stm.parse_sentence"
-      (str "Currently, the parsing api only supports parsing at the tip of the document.");
+      (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
+       str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
+       str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
+  if not (Stateid.equal sid real_tip) then
+    Feedback.msg_debug
+      (str "Warning, the real tip doesn't match the current tip." ++
+       str "You wanted to parse at: "  ++ str (Stateid.to_string sid) ++
+       str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++
+       str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++
+       str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
   Flags.with_option Flags.we_are_parsing (fun () ->
       try
         match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
@@ -2721,7 +2734,8 @@ let add ~ontop ?newtip verb (loc, ast) =
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
     user_err ~hdr:"Stm.add"
-      (str "You used Stm.add on a different state than the tip" ++ fnl () ++
+      (str "Stm.add called for a different state (" ++ str (Stateid.to_string ontop) ++
+       str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++
        str "This is not supported yet, sorry.");
   let indentation, strlen = compute_indentation ontop loc in
   CWarnings.set_current_loc loc;