diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-03-20 13:48:07 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-03-20 13:48:07 +0100 |
| commit | 364ea0c9d57df647af4f207d69eee002b2f8073e (patch) | |
| tree | 65b9de9140020fc04812ddbb2c541a92b138c249 | |
| parent | 0699adb9d3385b94077a51b5b6ddbd74ec45f6b9 (diff) | |
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.
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 1c1cb8e05..473065bed 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 |