From 36df9cd8eb5a793502896df82bc7291ae9c66d35 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 20 Aug 2010 09:59:38 +0000
Subject: Mention Fast Process Buffer

---
 CHANGES | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index 9426317d..194defc3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -31,11 +31,21 @@
     buffers can be ignored and hidden.  Use "full annotation" to keep
     output when several steps are taken.
 
-*** Automatic processing mode (experimental)
+*** Automatic processing mode
     Quick Options -> Send Automatically
     Sends commands to the prover when Emacs is idle for a while.
-    NB: EXPERIMENTAL this is in progress, currently too obtrusive 
-    to be usable.
+    This only sends commands when the last processing action has
+    been an action moving forward through the buffer.  Interrupt by
+    making a keyboard/mouse action.
+
+*** Fast buffer processing option
+    Quick Options -> Fast Process Buffer
+    This affects 'proof-process-buffer' (C-c C-b, toolbar down).
+    It causes commands to be sent to the prover in a tight loop, without 
+    updating the display or processing other input.  This speeds up
+    processing dramatically on some Emacs implementations.
+    To interrupt, use C-g, which reverts to normal processing mode.
+    (To stop that, use C-c C-c as usual).
 
 *** Improved prevention of Undo in locked region
     With thanks to Erik Martin-Dorel and Stefan Monnier.
-- 
cgit v1.2.3