aboutsummaryrefslogtreecommitdiff
path: root/html
diff options
context:
space:
mode:
authorDavid Aspinall1998-12-11 17:51:40 +0000
committerDavid Aspinall1998-12-11 17:51:40 +0000
commit4f4f7543d8317b6cba78c43671fc3c65658e7581 (patch)
treefb59dd89fcb60759fe01c2b8b11f323f2fc54b35 /html
parent2334f0e7c457283fb706a272a5cb97494c5563b6 (diff)
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?
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions