From 9c6ee4eae961e39a76fa02d395147c7b3eefd497 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 8 May 2007 12:40:14 +0000
Subject: tuned cannot-undo;

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

diff --git a/isar/isar.el b/isar/isar.el
index d37d5815..20365bb7 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -452,13 +452,10 @@ proof-shell-retract-files-regexp."
        ((and (proof-string-match isar-end-regexp str)
 	     (isar-command-nested span))
         (setq ans isar-undo))
-       ;; not undoable: fail and exit 
-       ;; [da: this is an odd case: it issues cannot_undo command to Isar,
-       ;;  which immediately generates an error, I think it's a bit confusing
-       ;; for the user]
+       ;; non-nested end: undoable in Isabelle2007
        ((and (proof-string-match isar-undo-fail-regexp str))
+        (setq ans (isar-cannot-undo (match-string 1 str)))
         (setq answers nil)
-        (setq ans (isar-cannot-undo str))
         (setq span nil))
        ;; theory: remove and exit
        ((proof-string-match isar-undo-remove-regexp str)
-- 
cgit v1.2.3