Skip to content

Commit

Permalink
Fixing #62.
Browse files Browse the repository at this point in the history
I don't know if it is a coq bug that bullet do not support Time. I
remove Time from bullets for the moment.
  • Loading branch information
Matafou committed Mar 8, 2016
1 parent 0443734 commit 60dcd96
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion coq/coq.el
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 60dcd96

Please sign in to comment.