isar-syntactic-context: modify proof-looking-at-syntactic-context to allow

recognition of terminating comment strings.

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