proof-looking-at (subject to proof-case-fold-search);

2 files changed, 23 insertions, 0 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 0e0f608a..1a5e0ad8 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2779,6 +2779,14 @@ This hook may be useful for synchronizing with the proof
 assistant, for example, to switch to a new theory
 (in case that isn't already done by commands in the proof
 script).
+
+When functions in this hook are called, the variable
+@samp{activated-interactively} will be non-nil if 
+@code{proof-activate-scripting} was called interactively
+(rather than as a side-effect of some other action).
+If a hook function sends commands to the proof process,
+it should wait for them to complete (so the queue is cleared
+for scripting commands), unless activated-interactively is set.
 @end defvar
 @c TEXI DOCSTRING MAGIC: proof-stack-to-indent
 @defvar proof-stack-to-indent 
@@ -4108,6 +4116,15 @@ To debug Proof General, it may be helpful to set the
 configuration variable @code{proof-show-debug-messages}.
 
 @c TEXI DOCSTRING MAGIC: proof-show-debug-messages
+@defopt proof-show-debug-messages 
+Whether to display debugging messages in the response buffer.@*
+If non-nil, debugging messages are displayed in the response giving
+information about what Proof General is doing.
+To avoid erasing the messages shortly after they're printed, 
+you should set @samp{@code{proof-tidy-response}} to nil.
+
+The default value is @code{t}.
+@end defopt
 
 For more information about debugging Emacs lisp, consult the Emacs Lisp
 Reference Manual.  I recommend using the source-level debugger
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 1d03131e..37819d8b 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -57,6 +57,12 @@ nil if a region cannot be found."
       ((case-fold-search proof-case-fold-search))
     (string-match regexp string start)))
 
+(defun proof-looking-at (regexp)
+  "Like looking-at, but set case-fold-search to proof-case-fold-search."
+  (let
+      ((case-fold-search proof-case-fold-search))
+    (looking-at regexp)))
+
 
 ;; Generic font-lock