From 346b2bf9593bee26e2d3d4f2319df38a92fe9112 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 19 Aug 2007 11:18:48 +0000
Subject: pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete
 closing markup (special 377).

---
 isar/isar.el | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/isar/isar.el b/isar/isar.el
index 9c717941..a1a73731 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -144,7 +144,7 @@ See -k option for Isabelle interface script."
 (defun isar-shell-mode-config-set-variables ()
   "Configure generic proof shell mode variables for Isabelle/Isar."
   (setq
-   pg-topterm-regexp			"\375\\|\^AV"
+   pg-topterm-regexp			"\376\\|\^AW"
 
    pg-topterm-goalhyplit-fn		'isar-goalhyplit-test
    proof-shell-wakeup-char              nil
@@ -635,10 +635,13 @@ Checks the width in the `proof-goals-buffer'"
   (proof-goals-config-done))
 
 (defun isar-goalhyplit-test ()
-  "This is a value for pg-topterm-goalhyplit-fn, see proof-config.el for docs."
+  "Value for `pg-topterm-goalhyplit-fn' (see that variable for documentation)."
   (let ((start (point)))
-    (and (proof-re-search-forward "\375\\|\^AW" nil t)
-      (cons 'lit (buffer-substring start (match-beginning 0))))))
+    (if (proof-re-search-forward "\377\\|\^AX" nil t) ;; end of literal command (non-standard)
+	(progn
+	  (delete-region (match-beginning 0) (match-end 0))
+	  (cons 'lit (buffer-substring start (match-beginning 0)))))))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-- 
cgit v1.2.3