aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar-syntax.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-17 13:42:50 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-17 13:42:50 +0000
commit2a144282a0b0a7109d7e9cf11f8881e6a0f203ef (patch)
treee8cf26c7e7c258a141448a54eb6e8e24fe1a064c /isar/isar-syntax.el
parent9bed9eb56b63db397fdb4b9a76197ffc4d150ff6 (diff)
isar-syntactic-context: modify proof-looking-at-syntactic-context to allow
recognition of terminating comment strings.
Diffstat (limited to 'isar/isar-syntax.el')
-rw-r--r--isar/isar-syntax.el10
1 files changed, 10 insertions, 0 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 68740351..912fcb7a 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -248,6 +248,16 @@ matches contents of quotes for quoted identifiers.")
(defconst isar-string-start-regexp "\"\\|`\\|{\\*")
(defconst isar-string-end-regexp "\"\\|`\\|\\*}")
+(defun isar-syntactic-context ()
+ (let ((sc (proof-looking-at-syntactic-context-default)))
+ (or (if (eq sc 'string)
+ (save-excursion
+ (save-match-data
+ (and (re-search-backward isar-string-start-regexp)
+ (re-search-backward "--")
+ 'comment))))
+ sc)))
+
;; antiquotations