diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-03-08 16:03:24 +0100 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-03-08 16:03:24 +0100 |
commit | 60dcd96a3efaff3cde5d11873ff82669d8dbe993 (patch) | |
tree | d38ddfce765e90bb617b1a4536db1ea4a7eb6b08 /coq/coq.el | |
parent | 0443734841b337b3695de02275b1a2500931358b (diff) |
Fixing #62.
I don't know if it is a coq bug that bullet do not support Time. I
remove Time from bullets for the moment.
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -1904,12 +1904,16 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (defconst coq--time-prefix "Time " "Coq command prefix for displaying timing information.") +(defun coq-bullet-p (s) + (string-match coq-bullet-regexp-nospace s)) + ;; Remark: `action' and `string' are known by `proof-shell-insert-hook' (defun coq-preprocessing () (when coq-time-commands (with-no-warnings ;; NB: dynamic scoping of `string' and `action' ;; Don't add the prefix if this is a command sent internally - (unless (eq action 'proof-done-invisible) + (unless (or (eq action 'proof-done-invisible) + (coq-bullet-p string)) ;; coq does not accept "Time -". (setq string (concat coq--time-prefix string)))))) (add-hook 'proof-shell-insert-hook 'coq-preprocessing) |