From 364ea0c9d57df647af4f207d69eee002b2f8073e Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 20 Mar 2015 13:48:07 +0100
Subject: Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.

In PG there are shortcuts that perform on the fly "Set Printing
All"/"Unset Printing All" in pg. For example if you type C-u before
some shortcut for print (check/About/Show), it performs:

Set Printing All.
Print foo.
Unset Printing All.

But if the "Unset" prints a goal, then pg interprets the output of
Print as a command applied on a previous line, and thus hides it.

So for emacs mode I would prefer no goal printing when options are
set/unset. In the situation where this should be done (when setting
durably the option probably), I'd rather program a "Show" explicitely.
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 1c1cb8e05c..473065bedc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2367,7 +2367,7 @@ let interp verb (_,e as lexpr) =
       verb && match clas with
        | VtQuery _, _ -> false
        | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
-       | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
+       | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
       let e = Errors.push e in
-- 
cgit v1.2.3