| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-11-15 | Fixed mistake in function names. Tidied menus a bit | David Aspinall | |
| 1999-11-15 | Fixes for FSF overlay obscurity. | David Aspinall | |
| 1999-11-15 | Reorganization of user-level commands, code moved from proof-toolbar.el | David Aspinall | |
| 1999-11-15 | Reorganization and cleanup of key-bindings. | David Aspinall | |
| FSF fix for proof-cd. Fix for proof-goto-point. Made proof-done-advancing robust against unset proof-save-command-regexp. Improved several docstrings. Fixes for proof-frob-locked end, made disabled by default for novices. Fix for electric terminator indicator in non-PG buffers. Configuration variable proof-font-lock-zap-commas. Removed proof-try-command. Phew! | |||
| 1999-11-14 | Fixes for proof-goto-commmand-{end,start}. Former new function | David Aspinall | |
| 1999-11-14 | Many robustness improvements for error and interrupt handling: | David Aspinall | |
| - 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) | |||
| 1999-11-14 | proof-nested-goals-allowed -> proof-completed-proof-behaviour | David Aspinall | |
| Patch for more flexible handling of closing goal...save regions after proof has been completed. | |||
| 1999-11-13 | Beginnings of improved version of goal..no save regions. | David Aspinall | |
| 1999-11-12 | Fixes for Isabelle in case theory file is visited before script file. | David Aspinall | |
| 1999-11-11 | Next round of fixups for font-lock and x-symbol. | David Aspinall | |
| 1999-11-11 | Extensive fixes for x-symbol and font-lock. | David Aspinall | |
| 1999-11-11 | Added proof-help command to help menu. | David Aspinall | |
| 1999-11-11 | Added new command proof-goto-point, new default binding for C-c RET. | David Aspinall | |
| 1999-11-10 | Added some desparate patches for dead extent problem proof-done-advancing | David Aspinall | |
| 1999-11-10 | Reorganized user options. Special new code for boolean settings. | David Aspinall | |
| 1999-11-10 | fixed indentation bug: use proof-looking-at (proof-case-fold-search); | Makarius Wenzel | |
| 1999-11-10 | Moved proof-file-truename, proof-file-to-buffer, to proof.el | David Aspinall | |
| Made setting font-lock-always-fontify-immediately be buffer local in proof scripts (it's an ugly hack for comma-defontification). | |||
| 1999-11-09 | Generic support for x-symbol tuned up. | David Aspinall | |
| 1999-11-09 | Bug again in call-interactively in proof-toggle-active-scripting. | David Aspinall | |
| Turn on proof-x-symbol mode in proof script mode. | |||
| 1999-11-09 | Bug in proof-toggle-active-scripting interactive calling. | David Aspinall | |
| 1999-11-09 | Arrange for activate-scripting to not block for interactive calls. | David Aspinall | |
| 1999-11-08 | proof-prf-string -> proof-showproof-command | David Aspinall | |
| 1999-11-08 | Comments/messages. | David Aspinall | |
| 1999-11-08 | Copyright messages updated. | David Aspinall | |
| 1999-10-27 | tuned msg; | Makarius Wenzel | |
| 1999-10-25 | Implementation of proof-auto-multiple-files. | David Aspinall | |
| 1999-10-21 | Added symmetric proof-shell-inform-file-retracted-cmd setting to correspond | David Aspinall | |
| with the state change of a buffer from completely processed to partly processed. | |||
| 1999-10-21 | Changed name of proof-shell-cd-cmd for uniformity. | David Aspinall | |
| 1999-10-21 | Changed name to proof-shell-inform-file-processed-cmd | David Aspinall | |
| 1999-10-21 | Added proof-shell-inform-file-processed-command setting. | David Aspinall | |
| 1999-10-20 | Comments in proof-complete-buffer-atomic. | David Aspinall | |
| 1999-10-19 | Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic. Fix to only ↵ | David Aspinall | |
| close off to (proof-script-end), not (point-max). | |||
| 1999-10-18 | Missing cursor move | David Aspinall | |
| 1999-10-15 | FIRST ATTEMPT AT CANY QUEUE HANDLING. Extending regions when advancing patch. | David Aspinall | |
| 1999-10-14 | Fix missing save-excursion causing bug with proof-process-buffer. | David Aspinall | |
| 1999-10-07 | Fix for older emacsen, maybe. | David Aspinall | |
| 1999-10-06 | Tidy proof-interrupt-process | David Aspinall | |
| 1999-10-06 | Speed optimizations, part I. | David Aspinall | |
| 1999-10-06 | More improvements/fixes for closing unfinished proofs. | David Aspinall | |
| Added proof-unnamed-theorem-name. | |||
| 1999-10-06 | Made new command proof-cd to cd to the directory of the current | David Aspinall | |
| buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly. | |||
| 1999-10-06 | Support for closing off incomplete goal-saves. | David Aspinall | |
| 1999-10-06 | Cleaned up. Fixed bug in proof-queue-or-locked-end | David Aspinall | |
| 1999-10-06 | BUG 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-06 | remove dead code | David Aspinall | |
| 1999-10-06 | proof-try-command is deprecated | David Aspinall | |
| 1999-10-06 | Updates. | David Aspinall | |
| 1999-10-06 | Added 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-01 | Fixup name changes | David Aspinall | |
| 1999-10-01 | Renamed some configuration variables for uniformity, see CHANGES. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |