From ad3cf74615236f4fb5dd57e2dc599256c825f093 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 11 Dec 1998 17:15:11 +0000
Subject: Allow even the current scripting buffer to be marked atomically in
 case the prover asks it to be.  This can happen when loading theory files in
 Isabelle.

---
 generic/proof-script.el | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index a95abda7..febb29e6 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -347,19 +347,9 @@ to allow other files loaded by proof assistants to be marked read-only."
 				      " have not been saved!")))
 	  (setq proof-included-files-list
 		(cons cfile proof-included-files-list))
-	  ;; If the file is loaded into a buffer, which isn't
-	  ;; the current scripting buffer, then put an
+	  ;; If the file is loaded into a buffer, put an
 	  ;; atomic locked region in it.
-
-	  ;; FIXME da: I don't think we should skip the scripting
-	  ;; buffer!  Perhaps this was just added as a hack for
-	  ;; Isabelle's broken theory mechanism?
-	  (if (and buffer
-		   (if proof-script-buffer
-		       (not (equal cfile
-				   (file-truename 
-				    (buffer-file-name proof-script-buffer))))
-		     t))
+	  (if buffer
 	      (proof-mark-buffer-atomic buffer))))))
 
 (defun proof-unregister-buffer-file-name ()
-- 
cgit v1.2.3