|
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?
|
