diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-19 11:09:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-19 11:09:08 +0000 |
| commit | 5e56cfc4cc792dfad7dcb578fdccc48ba0196851 (patch) | |
| tree | 9aa1d6a20196a236e4b2ab28e6841d756a2a95ca /generic/pg-user.el | |
| parent | ed11ccb7b647582296c0ddd8023f180ad591e15b (diff) | |
Add Fast Process Buffer option
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index d884594c..60ba77b1 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -194,8 +194,11 @@ If inside a comment, just process until the start of the comment." (save-excursion (goto-char (point-max)) (proof-assert-until-point-interactive)) - (proof-maybe-follow-locked-end))) - + (proof-maybe-follow-locked-end)) + (when proof-fast-process-buffer + (message "Processing buffer...") + (proof-shell-wait) + (message "Processing buffer...done"))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |