aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el17
1 files changed, 1 insertions, 16 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)))
-
-
-
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;