Goal printing made uniform: always done in STM (close 3585)

Goal printing was partially broken.  Some commands in vernacentries
were printing, but not all of them.  Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.

Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs.  More modern GUI do ask for the goals.

4 files changed, 24 insertions, 29 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index a744ce9b0b..d94482cebf 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -8,7 +8,7 @@
 
 let with_option o f x =
   let old = !o in o:=true;
-   try let r = f x in o := old; r
+   try let r = f x in if !o = true then o := old; r
    with reraise ->
      let reraise = Backtrace.add_backtrace reraise in
      let () = o := old in
@@ -27,7 +27,7 @@ let with_options ol f x =
 
 let without_option o f x =
   let old = !o in o:=false;
-  try let r = f x in o := old; r
+  try let r = f x in if !o = false then o := old; r
   with reraise ->
     let reraise = Backtrace.add_backtrace reraise in
     let () = o := old in
diff --git a/stm/stm.ml b/stm/stm.ml
index 74a998a74f..78f7682a39 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1589,6 +1589,9 @@ let observe id =
 
 let finish () =
   observe (VCS.get_branch_pos (VCS.current_branch ()));
+  if (not !Flags.print_emacs && !Flags.coqtop_ui && not !Flags.batch_mode) ||
+     (!Flags.print_emacs && Flags.is_verbose ()) then
+    Pp.msg_notice (pr_open_cur_subgoals ());
   VCS.print ()
 
 let wait () =
@@ -1697,7 +1700,7 @@ let reset_task_queue = Slaves.reset_task_queue
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
   let warn_if_pos a b =
     if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
-  let v, x = expr, { verbose = verbose && Flags.is_verbose(); loc; expr } in
+  let v, x = expr, { verbose = verbose; loc; expr } in
   prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
   let vcs = VCS.backup () in
   try
@@ -1738,9 +1741,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           VCS.commit id (Alias oid);
-          if (!Flags.coqtop_ui && not !Flags.batch_mode) ||
-             !Flags.print_emacs then
-            Pp.msg_notice (pr_open_cur_subgoals ());
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
           prerr_endline ("undo to state " ^ Stateid.to_string id);
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b56b515dc6..2edc9759e2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -289,7 +289,7 @@ let checknav loc ast =
   if is_deep_navigation_vernac ast then
     user_error loc "Navigation commands forbidden in nested commands"
 
-let eval_expr loc_ast = vernac_com true checknav loc_ast
+let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 816912be40..74ea904c4a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -438,9 +438,7 @@ let vernac_notation locality local =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print k l hook =
-  start_proof_com k l hook;
-  print_subgoals ()
+let start_proof_and_print k l hook = start_proof_com k l hook
 
 let no_hook = Lemmas.mk_hook (fun _ _ -> ())
 
@@ -814,7 +812,6 @@ let vernac_solve n tcom b =
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus command_focus p in
     p,status) in
-    print_subgoals();
     if not status then Pp.feedback Feedback.AddedAxiom
  
 
@@ -1647,13 +1644,12 @@ let vernac_focus gln =
       | Some 0 ->
          Errors.error "Invalid goal number: 0. Goal numbering starts with 1."
       | Some n ->
-         Proof.focus focus_command_cond () n p);
-  print_subgoals ()
+         Proof.focus focus_command_cond () n p)
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus () =
-  Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus command_focus p ());
-  print_subgoals ()
+  Proof_global.simple_with_current_proof
+    (fun _ p -> Proof.unfocus command_focus p ())
 
 (* Checks that a proof is fully unfocused. Raises an error if not. *)
 let vernac_unfocused () =
@@ -1677,20 +1673,15 @@ let vernac_subproof gln =
   Proof_global.simple_with_current_proof (fun _ p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
-    | Some n -> Proof.focus subproof_cond () n p);
-  print_subgoals ()
+    | Some n -> Proof.focus subproof_cond () n p)
 
 let vernac_end_subproof () =
-  Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ());
-  print_subgoals ()
-
+  Proof_global.simple_with_current_proof (fun _ p ->
+    Proof.unfocus subproof_kind p ())
 
 let vernac_bullet (bullet:Proof_global.Bullet.t) =
   Proof_global.simple_with_current_proof (fun _ p ->
-    Proof_global.Bullet.put p bullet);
-  (* Makes the focus visible in emacs by re-printing the goal. *)
-  if !Flags.print_emacs then print_subgoals ()
-
+    Proof_global.Bullet.put p bullet)
 
 let vernac_show = function
   | ShowGoal goalref ->
@@ -1904,11 +1895,11 @@ let interp ?proof locality poly c =
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) -> print_subgoals ()
-  | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals ()
-  | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals ()
+  | VernacProof (None, None) -> ()
+  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
+  | VernacProof (None, Some l) -> vernac_set_used_variables l
   | VernacProof (Some tac, Some l) -> 
-      vernac_set_end_tac tac; vernac_set_used_variables l ; print_subgoals ()
+      vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
   | VernacToplevelControl e -> raise e
@@ -2062,7 +2053,11 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             Flags.program_mode := orig_program_mode
           end
         with
-          | reraise when (match reraise with Timeout -> true | e -> Errors.noncritical e) ->
+        | reraise when
+              (match reraise with
+              | Timeout -> true
+              | e -> Errors.noncritical e)
+          ->
             let e = Errors.push reraise in
             let e = locate_if_not_already loc e in
             let () = restore_timeout () in