diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-02-28 19:20:11 -0500 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2016-02-28 19:22:46 -0500 |
| commit | 11b03d47628bf833e98e0b3d8ae9c5c9a358235d (patch) | |
| tree | 30c4bc158b8941e6ba63f06750a11bfa53fae062 /coq/coq.el | |
| parent | 81691ff03d8a13185a829d9975c59e0f5ebdd6aa (diff) | |
Don't add the ‘Time’ prefix to internal Coq commands
This ensures that parts of Proof General that use Coq commands in the
background are not confused by extra timing information.
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -1906,9 +1906,11 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." ;; Remark: `action' and `string' are known by `proof-shell-insert-hook' (defun coq-preprocessing () - (if coq-time-commands + (when coq-time-commands + ;; Don't add the prefix if this is a command sent internally + (unless (memq 'no-response-display proof-shell-delayed-output-flags) (with-no-warnings ;; NB: dynamic scoping of `string' - (setq string (concat coq--time-prefix string))))) + (setq string (concat coq--time-prefix string)))))) (add-hook 'proof-shell-insert-hook 'coq-preprocessing) |