| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Unify goals and response menus with script buffer menu
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof-shell-invisible-command: add terminator if it seems to be
missing (after all: it's useful for users with C-c C-v).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
issue with non-mule FSF Emacs (that was something different).
|
|
|
|
|
|
|
|
jrl's bug report about duplication of occasional urgent messages.
The correct fix is to set proof-shell-eager-annotation-start-length
properly.
|
|
functions.
|
|
|
|
|
|
|
|
add function for new multiple frames user option.
Don't display "done" in goals buffer (may never happen anyway)
Remove code for response buffer erasing.
Clean some comments.
|
|
|
|
|
|
|
|
|
|
fix 'no-catch for exited tag' buglet.
|
|
|
|
Fix to proof-shell-insert-loopback-cmd for pbp.
Don't call pbp-make-top-span if proof-goal-hyp-fn is unset.
Remove extra newline in goals output.
Removed some dead code.
Made code robust against more settings being unset.
Added menu to goals buffer.
Set key "q" in response and goals buffers to bury-buffer.
Quit timeout variable.
|
|
|
|
Docstring and debug msgs
|
