Disabled hack for proof-shell-process-file which allowed

empty string to stand for filename of current scripting buffer.
This added the current script buffer onto the included files
list immediately processing it began (if it began with something
creating a mark).  However, I removed the check for the current
scripting buffer so that that could correctly be marked atomic
for Isabelle at other times.  This resulted in current buffer
being marked atomic, and errors.
Are there still more errors?

1 files changed, 11 insertions, 3 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index df117c79..7bb5c6e0 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1063,9 +1063,17 @@ if none of these apply, display."
 	((file (funcall (cdr proof-shell-process-file) message)))
       ;; Special hack: empty string indicates current scripting buffer
       ;; (not used anywhere presently?)
-      (if (and proof-script-buffer (string= file ""))
-	  (setq file (buffer-file-name proof-script-buffer)))
-      (if file
+      ;; (if (and proof-script-buffer (string= file ""))
+      ;;  (setq file (buffer-file-name proof-script-buffer)))
+      ;; YES!  It *was* used by LEGO.
+      ;; Now we avoid this in favour of altering the processed
+      ;; files list when the current scripting buffer changes,
+      ;; inside Proof General.  Attempt to harmonize behaviour
+      ;; with Isabelle.  Seems wrong to add "example.l" to
+      ;; list of processed files if it's only partly processed?
+      ;; (On the other hand, for lego, it may have declared a 
+      ;;  module heading).
+      (if (and file (not (string= file "")))
 	  (proof-register-possibly-new-processed-file file))))
 
    ;; Is the prover retracting across files?