| Age | Commit message (Collapse) | Author |
|---|
|
functionality now in Isabelle's update_thy for PG
|
|
Added switch off of simplifier tracing to quiet command
(not good enough -- need help from Isabelle for that really).
|
|
completion for x-symbol tokens.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
isa-set-default-cmd->isabelle-set..
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
fixed some comments;
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof-shell-filename-escapes, and always apply for filename substn.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof-shell-eager-annotation-start-length.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Introduce proof-shell-error-or-interrupt-seen flag set after an error
or interrupt was seen (in fact, on every call to proof-release-lock).
Examine it in proof-activate-scripting to see whether hooks succeeded
in activating scripting.
- Test in the shell filter for the lock being held yet nothing in the
action list, and clear the lock if so. Gets rid of repetetive
proof-shell-busy messages when the queue is empty (for errors during
development, or nasty uses of C-g)
- Add a timeout to proof-shell-wait (not used yet)
|
|
Patch for more flexible handling of closing goal...save regions
after proof has been completed.
|
