[toplevel] Restore 8.6 goal printing behavior.

When porting the toplevel to the STM, the logic for goal printing was
simplified too much under optimistic assumptions. The idea was not to
rely on the `vernac_classifier` which is an internal and complicated
beast.

However, it seems there are many cases to consider other than
`is_query`, so at the risk of reimplementing the classifier we revert
to the old approach of using the full classification.

This gives maximum 8.6 compatibility, with the pitfall of having to
call the classifier. Indeed, due to the dynamic nature of the "undo
classifier", we cannot call it after `Stm.add`, as the document tree
will be not the right one, making the classification of undo commands
incorrect (actually raising an error "Cannot undo").

1 files changed, 15 insertions, 4 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4fca4ea18..e79ee1a42 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,6 +124,16 @@ let rec interp_vernac sid (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
+
+      (* XXX: We need to run this before add as the classification is
+         highly dynamic and depends on the structure of the
+         document. Hopefully this is fixed when VtBack can be removed
+         and Undo etc... are just interpreted regularly. *)
+      let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
+        | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+        | _ -> false
+      in
+
       let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
@@ -137,11 +147,12 @@ let rec interp_vernac sid (loc,com) =
       if check_proof then Stm.finish ();
 
       (* We could use a more refined criteria that depends on the
-         vernac. For now we imitate the old approach. *)
-      let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
-                       not (Proof_global.there_are_pending_proofs ()) in
+         vernac. For now we imitate the old approach and rely on the
+         classification. *)
+      let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+                        is_proof_step && Proof_global.there_are_pending_proofs () in
 
-      if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+      if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
       nsid
   in
     try