added proof-looking-at-safe, proof-looking-at-syntactic-context;

removed proof-indent-commands-regexp;

1 files changed, 13 insertions, 8 deletions

diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 3da86f62..5f5eeb1a 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -53,9 +53,9 @@ nil if a region cannot be found."
 	(if (re-search-forward endre nil t)
 	    start))))
 
-;; Function for string matching that takes into account value
-;; of proof-case-fold-search.  Last arg to string-match is
-;; not applicable.
+;; Functions for string matching and searching that take into account
+;; value of proof-case-fold-search.  Last arg to string-match is not
+;; applicable.
 
 (defun proof-re-search-forward (regexp &optional bound noerror count)
   "Like re-search-forward, but set case-fold-search to proof-case-fold-search."
@@ -92,14 +92,19 @@ nil if a region cannot be found."
       ((case-fold-search proof-case-fold-search))
     (looking-at regexp)))
 
+(defun proof-looking-at-safe (regexp)
+  "Like proof-looking-at, but return nil if REGEXP is nil."
+  (if regexp (proof-looking-at regexp)))
 
-;; Generic font-lock
+(defun proof-looking-at-syntactic-context ()
+  "Determine if current point is at beginning or within comment/string context."
+  (or
+   (buffer-syntactic-context)
+   (proof-looking-at-safe proof-comment-start-regexp)
+   (proof-looking-at-safe proof-string-start-regexp)))
 
-(defvar proof-indent-commands-regexp ""
-  "Subset of keywords and tacticals which are terminated by the
-`proof-terminal-char'.  Basic indentation is provided automatically
-for these.")
 
+;; Generic font-lock
 
 (defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"
   "A regular expression for parsing identifiers.")