[toplevel] Modify printing goal strategy.

Instead of using a command-analysis heuristic, coqtop will now print
goals if the goal has changed. We use a fast goal comparison
heuristic, but a more refined strategy would be possible.

This brings some [IMHO very welcome] change to PG and `-emacs`, which
will now disable the printing of goals. Now, instead of playing with
`Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show`
command whenever it wishes to redisplay the goals.

This change will break PG, so we need to carefully coordinate this PR
with PG upstream (see ProofGeneral/PG#212).

Some interesting further things to do:

- Detect changes in nested proofs.
- Uncouple the silent flag from "print goals".

2 files changed, 22 insertions, 31 deletions

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 1da46e8ce..a103cfe7f 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -341,6 +341,22 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
+let pr_open_cur_subgoals () =
+  try
+    let proof = Proof_global.give_me_the_proof () in
+    Printer.pr_open_subgoals ~proof
+  with Proof_global.NoCurrentProof -> Pp.str ""
+
+(* Goal equality heuristic. *)
+let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
+let evleq e1 e2 = CList.equal Evar.equal e1 e2
+let cproof p1 p2 =
+  let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in
+  evleq a1 b1 &&
+  CList.equal (pequal evleq evleq) a2 b2 &&
+  CList.equal Evar.equal a3 b3 &&
+  CList.equal Evar.equal a4 b4
+
 let drop_last_doc = ref None
 
 let rec loop ~time ~state =
@@ -351,6 +367,10 @@ let rec loop ~time ~state =
     (* Be careful to keep this loop tail-recursive *)
     let rec vernac_loop ~state =
       let nstate = do_vernac ~time ~state in
+      let proof_changed = not (Option.equal cproof nstate.proof state.proof) in
+      let print_goals = not !Flags.quiet &&
+                        proof_changed && Proof_global.there_are_pending_proofs () in
+      if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
       loop_flush_all ();
       vernac_loop ~state:nstate
     (* We recover the current stateid, threading from the caller is
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7c889500a..56bdcc7e5 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,12 +70,6 @@ let print_cmd_header ?loc com =
   Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com);
   Format.pp_print_flush !Topfmt.std_ft ()
 
-let pr_open_cur_subgoals () =
-  try
-    let proof = Proof_global.give_me_the_proof () in
-    Printer.pr_open_subgoals ~proof
-  with Proof_global.NoCurrentProof -> Pp.str ""
-
 (* Reenable when we get back to feedback printing *)
 (* let is_end_of_input any = match any with *)
 (*     Stm.End_of_input -> true *)
@@ -94,23 +88,8 @@ end
 let interp_vernac ~time ~check ~interactive ~state (loc,com) =
   let open State in
     try
-      (* 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 VtMeta can be removed
-         and Undo etc... are just interpreted regularly. *)
-
-      (* XXX: The classifier can emit warnings so we need to guard
-         against that... *)
-      let wflags = CWarnings.get_flags () in
-      CWarnings.set_flags "none";
-      let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with
-        | VtProofStep _ | VtMeta | VtStartProof _ -> true
-        | _ -> false
-      in
-      CWarnings.set_flags wflags;
-
-      (* The -time option is only supported from console-based
-         clients due to the way it prints. *)
+      (* The -time option is only supported from console-based clients
+         due to the way it prints. *)
       if time then print_cmd_header ?loc com;
       let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in
       let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in
@@ -123,14 +102,6 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) =
          it otherwise reveals bugs *)
       (* Stm.observe nsid; *)
       let ndoc = if check then Stm.finish ~doc else doc in
-
-      (* We could use a more refined criteria that depends on the
-         vernac. For now we imitate the old approach and rely on the
-         classification. *)
-      let print_goals = interactive && not !Flags.quiet &&
-                        is_proof_step && Proof_global.there_are_pending_proofs () in
-
-      if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
       let new_proof = Proof_global.give_me_the_proof_opt () in
       { doc = ndoc; sid = nsid; proof = new_proof }
     with reraise ->