| Age | Commit message (Collapse) | Author |
|---|
|
|
|
with the state change of a buffer from completely processed to
partly processed.
|
|
|
|
|
|
|
|
|
|
close off to (proof-script-end), not (point-max).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Added proof-unnamed-theorem-name.
|
|
buffer. Added a version of it to proof-activate-scripting-hook.
Removed cd from initialization sequence.
Changed prover specifics accordingly.
|
|
|
|
|
|
|
|
proof-deactivate-scripting: new implementation which allows user
choice of retraction or assertion. Forms a subroutine of
proof-activate-scripting.
proof-activate-scripting:
call proof-activate-scripting-hook *after* files are saved.
proof-mark-buffer-atomic: set proof-locked end to proof-script-end,
not (point-max).
New functions: proof-toggle-scripting, proof-auto-deactivate-scripting,
proof-script-end
|
|
|
|
|
|
|
|
Added question to user when switching scripting buffer,
and new option proof-auto-retract-other-buffers to disable question.
This reimplements the old "steal scripting?" idea.
|
|
|
|
|
|
|
|
restart).
|
|
|
|
C-button1
|
|
|
|
|
|
|
|
Added extra doc strings to hair macro definitions of functions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Check that there is active scripting buffer, in Isabelle there might not be.
|
|
proof-string-end-regexp;
|
|
more general qed schemes, such as Isabelle/Isar's nested proofs;
|
|
|
|
|
|
|
