diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 17:15:11 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 17:15:11 +0000 |
commit | ad3cf74615236f4fb5dd57e2dc599256c825f093 (patch) | |
tree | 56eedbecc0836a2ae672278d0826349ca65a417a /generic/proof-script.el | |
parent | 1a10f19e8a61388e74ecc60bf603753cb06681fe (diff) |
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.
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r-- | generic/proof-script.el | 14 |
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 () |