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.

1 files changed, 2 insertions, 12 deletions

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 ()