aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Collapse)Author
1999-10-06Cleaned up. Fixed bug in proof-queue-or-locked-endDavid Aspinall
1999-10-06BUG FIX: hopefully fixed spurious locked region problem.David Aspinall
1999-10-06 docstring and error message improvements.David Aspinall
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
1999-10-06remove dead codeDavid Aspinall
1999-10-06proof-try-command is deprecatedDavid Aspinall
1999-10-06Updates.David Aspinall
1999-10-06Added proof-retract-buffer symmetric to proof-process-buffer.David Aspinall
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.
1999-10-01Fixup name changesDavid Aspinall
1999-10-01Renamed some configuration variables for uniformity, see CHANGES.David Aspinall
1999-10-01Removed dubious 'dont own process' error in proof-interrupt-process.David Aspinall
1999-09-29Fixes so that proof-strict-read-only can be toggled within a session (via ↵David Aspinall
restart).
1999-09-29Changed name of proof-copy-span to proof-mouse-track-insert.David Aspinall
1999-09-29Re-enabled and renamed proof-send-span: becomes proof-copy-span bound to ↵David Aspinall
C-button1
1999-09-28More reorganizing of menus and keybindings with aim of usability in mind.David Aspinall
1999-09-28Reorganization of menus: made a single menu but flattened Scripting submenu.David Aspinall
1999-09-28Made Scripting menu entry item on menubar.David Aspinall
1999-09-23Added menu binding for finding theorems.David Aspinall
Added extra doc strings to hair macro definitions of functions.
1999-09-23Added proof-find-theorems and some hairy macros to define related commands.David Aspinall
1999-09-22Whitespace.David Aspinall
1999-09-22CommentsDavid Aspinall
1999-09-21Call proof-state-change-hook after asserting and retracting.David Aspinall
1999-09-13Removed proof-shell-completed added to eval-when-compile by mistake.David Aspinall
1999-09-13Added callbacks to refresh toolbarDavid Aspinall
1999-09-13Changed peculiar message to something slightly less peculiarDavid Aspinall
1999-09-13Experimental fix for proof-shell-completed flag clearing.David Aspinall
1999-09-13Added proof-terminal-string to proof-execute-minibuffer-cmd.David Aspinall
1999-09-03da: improved comment;Makarius Wenzel
1999-08-24Attempted fix of FSFmacs problem, left as commentDavid Aspinall
1999-08-20proof-goto-end-of-locked-if-pos-not-visible-in-window:David Aspinall
Check that there is active scripting buffer, in Isabelle there might not be.
1999-05-27improved proof-segment-up-to to support proof-string-start-regexp,Makarius Wenzel
proof-string-end-regexp;
1999-05-25proof-done-advancing: added proof-really-save-command-p to supportMakarius Wenzel
more general qed schemes, such as Isabelle/Isar's nested proofs;
1999-05-11Add toggle for proof toolbar to menuDavid Aspinall
1999-02-22Fixed bug by shifting configuration of minor mode for active terminator.David Aspinall
1999-02-01Used proof-string-match for matching against proof script.David Aspinall
1998-12-16Removed info file name space, again, arrgggh.David Aspinall
1998-12-16Added back space in info file nameDavid Aspinall
1998-12-16Reverted to previous semanticsDavid Aspinall
1998-12-16Made delete-region arg optional for proof-retract-until-point-interactive.David Aspinall
1998-12-16Removed space from ProofGeneral name.David Aspinall
1998-12-16Tweaked docstring for C-c C-u.David Aspinall
1998-12-16rationalised keybinding (again)Thomas Kleymann
1998-12-16improved default keybindingsThomas Kleymann
1998-12-15Docstring fixDavid Aspinall
1998-12-15Removed bogus duplicate call of proof-mode-hook at end of proof-config-done.David Aspinall
1998-12-15Fixes for FSF Emacs handling of processes, kill buffer hooks,David Aspinall
and live/dead overlays.
1998-12-15made many minor changes to the documentationThomas Kleymann
1998-12-11CommentsDavid Aspinall
1998-12-11Allow even the current scripting buffer to be marked atomicallyDavid Aspinall
in case the prover asks it to be. This can happen when loading theory files in Isabelle.
1998-12-11Several changes:David Aspinall
1. save-some-buffers now skips the current active scripting buffer. It was annoying to be asked whether to save this one as the user may have just begun typing into a fresh file, or may want to experiment with a modified proof, for example. 2. proof-deactivate-scripting improved so it works pretty well as a (so far undocumented) command. Kill buffer function now removes spans, so that they remain if we deactivate without killing. Plan is to call this in proof-activate-scripting to turn off current scripting buffer and munge the processed file list the way we like it. 3. In both proof-deactivate-scripting and proof-activate-scripting, we do the same thing: files with empty locked regions are removed from the processed files list, those with full locked regions are added. This is an attempt to harmonize the file handling of the theorem prover and whatever it reports with the scripting inside Proof General. Additionally proof-deactivate-scripting retracts a file with a partly locked region, only the active scripting buffer is allowed such a region (currently).
1998-12-11Added submit bug report to proof-shared-menuDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:21:06 +0000