aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-autotest.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-08 14:16:03 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-08 14:16:03 +0000
commit5f142a968a4a564cb2c0422d51bba4254f7c8d5e (patch)
tree2bdea10deff1ffb6efcbc4c1ad1c7fee14ab2dd4 /generic/pg-autotest.el
parentfc2a22ab7926da663de15b1fad1eccb45145e6db (diff)
Add timestamps. Fix random jump spurious error.
Diffstat (limited to 'generic/pg-autotest.el')
-rw-r--r--generic/pg-autotest.el9
1 files changed, 7 insertions, 2 deletions
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index fb52ebf1..3e9f2961 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -84,7 +84,9 @@
(save-excursion
(find-file file)
(erase-buffer)
- (setq pg-autotest-log (current-buffer))))
+ (setq pg-autotest-log (current-buffer))
+ (pg-autotest-message (concat "Tests started "
+ (format-time-string "%D %H:%M")))))
(defun pg-autotest-message (msg &rest args)
"Give message MSG in log file output and on display."
@@ -116,6 +118,8 @@
(defun pg-autotest-exit ()
"Exit Emacs returning Unix success 0 if all tests succeeded."
+ (pg-autotest-message (concat "\nTests completed "
+ (format-time-string "%D %H:%M")))
(proof-with-current-buffer-if-exists
pg-autotest-log
(save-buffer 0))
@@ -167,7 +171,8 @@ completely processing the buffer as the last step."
(pg-autotest-message
" random jump to point: %d" random-point)
(goto-char random-point)
- (unless (proof-only-whitespace-to-locked-region-p)
+ (unless (if (>= (point) (proof-unprocessed-begin))
+ (proof-only-whitespace-to-locked-region-p))
(proof-goto-point)
(proof-shell-wait) ;; TODO: check no prover error.
(decf jumps))))