Bring syntactic context functions together

4 files changed, 53 insertions, 66 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 8dbf2d14..069b7046 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1915,7 +1915,7 @@ that these may be overwritten)."
     (proof-extend-queue lastpos vanillas)))
 
 (defun proof-retract-before-change (beg end)
-  "For `before-change-functions'.  Retract to BEG unless BEG..END in comment.
+  "For `before-change-functions'.  Retract to BEG unless BEG and END in comment.
 No effect if prover is busy."
   (and (> (proof-queue-or-locked-end) beg)
        (not (and (proof-inside-comment beg)
@@ -1926,21 +1926,6 @@ No effect if prover is busy."
 	   (goto-char beg)
 	   (proof-retract-until-point)))))
 
-(defun proof-inside-comment (pos)
-  "Return non-nil if POS is inside a comment."
-  (save-excursion
-    (goto-char pos)
-    (eq (proof-buffer-syntactic-context) 'comment)))
-
-(defun proof-inside-string (pos)
-  "Return non-nil if POS is inside a comment."
-  (save-excursion
-    (goto-char pos)
-    (eq (proof-buffer-syntactic-context) 'string)))
-
-
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 9775002d..accd41de 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -108,6 +108,32 @@ nil if a region cannot be found."
   "Like `proof-looking-at', but return nil if REGEXP is nil."
   (if regexp (proof-looking-at regexp)))
 
+;;
+;; Syntactic context
+;;
+
+;; A function named after one in XEmacs
+(defun proof-buffer-syntactic-context (&optional buffer)
+  "Return the syntactic context of BUFFER at point.
+If BUFFER is nil or omitted, the current buffer is assumed.
+The returned value is one of the following symbols:
+
+	nil		; meaning no special interpretation
+	string		; meaning point is within a string
+	comment		; meaning point is within a line comment"
+  (save-excursion
+    (if buffer (set-buffer buffer))
+    (let ((pp (syntax-ppss)))
+	   ;;(parse-partial-sexp (point-min) (point))))
+      (cond
+       ((nth 3 pp) 'string)
+       ;; ((nth 7 pp) 'block-comment)
+       ;; "Stefan Monnier" <monnier+misc/news@rum.cs.yale.edu> suggests
+       ;; distinguishing between block comments and ordinary comments
+       ;; is problematic: not what XEmacs claims and different to what
+       ;; (nth 7 pp) tells us in GNU Emacs.
+       ((nth 4 pp) 'comment)))))
+
 (defsubst proof-looking-at-syntactic-context-default ()
   "Default function for `proof-looking-at-syntactic-context'."
   (or
@@ -117,7 +143,30 @@ nil if a region cannot be found."
    (save-match-data
      (when (proof-looking-at-safe proof-string-start-regexp) 'string))))
 
+(defun proof-looking-at-syntactic-context ()
+  "Determine if current point is at beginning or within comment/string context.
+If so, return a symbol indicating this ('comment or 'string).
+This function invokes <PA-syntactic-context> if that is defined, otherwise
+it calls `proof-looking-at-syntactic-context'."
+  (if (fboundp (proof-ass-sym syntactic-context))
+      (funcall (proof-ass-sym syntactic-context))
+    (proof-looking-at-syntactic-context-default)))
+
+(defun proof-inside-comment (pos)
+  "Return non-nil if POS is inside a comment."
+  (save-excursion
+    (goto-char pos)
+    (eq (proof-buffer-syntactic-context) 'comment)))
+
+(defun proof-inside-string (pos)
+  "Return non-nil if POS is inside a comment."
+  (save-excursion
+    (goto-char pos)
+    (eq (proof-buffer-syntactic-context) 'string)))
+
+;;
 ;; Replacing matches
+;;
 
 (defsubst proof-replace-string (string to-string)
   "Non-interactive `replace-string', using `proof-case-fold-search'."
@@ -135,7 +184,9 @@ nil if a region cannot be found."
     (while (proof-re-search-forward regexp nil t)
       (replace-match to-string nil nil))))
 
+;;
 ;; Generic font-lock
+;;
 
 (defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"
   "A regular expression for parsing identifiers.")
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 1d3932e9..a20106b0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -698,23 +698,6 @@ If optional arg REALLY-WORD is non-nil, it finds just a word."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Syntactic context
-;;
-
-;; [this belongs in proof-syntax but uses `proof-ass-sym' macro above]
-
-(defun proof-looking-at-syntactic-context ()
-  "Determine if current point is at beginning or within comment/string context.
-If so, return a symbol indicating this ('comment or 'string).
-This function invokes <PA-syntactic-context> if that is defined, otherwise
-it calls `proof-looking-at-syntactic-context'."
-  (if (fboundp (proof-ass-sym syntactic-context))
-      (funcall (proof-ass-sym syntactic-context))
-    (proof-looking-at-syntactic-context-default)))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
 ;; Stripping output and message
 ;;
 
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 4c77c34a..a9fae654 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -1,6 +1,6 @@
 ;; proof-compat.el   Operating system and Emacs version compatibility
 ;;
-;; Copyright (C) 2000-2009 LFCS Edinburgh.
+;; Copyright (C) 2000-2010 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -91,30 +91,6 @@ The value returned is the value of the last form in BODY."
 	   (progn ,@body)
 	 (select-frame ,old-frame))))))
 
-;; An implemenation of buffer-syntactic-context for GNU Emacs
-(defun proof-buffer-syntactic-context-emulate (&optional buffer)
-  "Return the syntactic context of BUFFER at point.
-If BUFFER is nil or omitted, the current buffer is assumed.
-The returned value is one of the following symbols:
-
-	nil		; meaning no special interpretation
-	string		; meaning point is within a string
-	comment		; meaning point is within a line comment"
-  (save-excursion
-    (if buffer (set-buffer buffer))
-    (let ((pp (syntax-ppss)))
-	   ;;(parse-partial-sexp (point-min) (point))))
-      (cond
-       ((nth 3 pp) 'string)
-       ;; ((nth 7 pp) 'block-comment)
-       ;; "Stefan Monnier" <monnier+misc/news@rum.cs.yale.edu> suggests
-       ;; distinguishing between block comments and ordinary comments
-       ;; is problematic: not what XEmacs claims and different to what
-       ;; (nth 7 pp) tells us in GNU Emacs.
-       ((nth 4 pp) 'comment)))))
-
-
-
 ;; These functions are used in the intricate logic around
 ;; shrink-to-fit.
 
@@ -158,14 +134,6 @@ The returned value is one of the following symbols:
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
-;;; General Emacs version compatibility
-;;;
-
-(defalias 'proof-buffer-syntactic-context
-	  'proof-buffer-syntactic-context-emulate)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
 ;;; Backward compatibility for Emacs 22
 ;;;