From 6818e58fece6dd2040fa32ff6fda7bf77d35c0d4 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 3 Oct 2009 16:31:30 +0000 Subject: proof-script-generic-parse-cmdstart: set case-fold-search proof-inside-string: added --- generic/proof-script.el | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'generic/proof-script.el') diff --git a/generic/proof-script.el b/generic/proof-script.el index 47564f12..3ca48ffd 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1710,6 +1710,7 @@ to the function which parses the script segment by segment." ;; ;; NB: proof-script-comment-start-regexp doesn't need to be the same ;; as (reqexp-quote comment-start). + (let ((case-fold-search proof-case-fold-search)) (if (looking-at proof-script-comment-start-regexp) ;; Find end of comment (if (proof-script-generic-parse-find-comment-end) 'comment) @@ -1745,7 +1746,7 @@ to the function which parses the script segment by segment." (skip-chars-backward " \t\n") ; benefit of the doubt, let 'cmd)))) ; the PA moan if it's incomplete ;; Return nil in other cases, no complete command found - ))))) + )))))) (defun proof-script-generic-parse-sexp () @@ -2080,6 +2081,7 @@ SEMIS must be a non-empty list, in reverse order (last position first). We assume that the list is contiguous and begins at (proof-queue-or-locked-end). We also delete help spans which appear in the same region (in the expectation that these may be overwritten)." + (assert semis nil "proof-assert-semis: argument must be a list") (proof-activate-scripting nil 'advancing) (let ((startpos (proof-queue-or-locked-end)) (lastpos (nth 2 (car semis))) @@ -2105,6 +2107,12 @@ No effect if prover is busy." (goto-char pos) (eq (proof-buffer-syntactic-context) 'comment))) +(defun proof-inside-string (pos) + "Returns non-nil if POS is inside a comment." + (save-excursion + (goto-char pos) + (eq (proof-buffer-syntactic-context) 'string))) + -- cgit v1.2.3