| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2000-05-11 | Use proof-deftoggle macro. | David Aspinall | |
| Comments about failure for ;;;###autoload cookie for define-derived-mode Attempted fixes for C-x C-w, C-x C-v, revert-buffer. | |||
| 2000-05-09 | Fixup loading. | David Aspinall | |
| 2000-05-09 | Removed menus, keybinding. Removed compatibility hacks. Improved loading. | David Aspinall | |
| 2000-05-05 | Comments. Minor improvements for electric terminator and ↵ | David Aspinall | |
| proof-follow-mode='ignore | |||
| 2000-05-02 | Added proof-assistant-keymap and commands for defining insert keys. | David Aspinall | |
| 2000-05-01 | Added proof-assistant-menu-entries for proof assistant specific menus. | David Aspinall | |
| 2000-04-25 | Note about efficiency/bug fix by Markus. | David Aspinall | |
| 2000-04-15 | proof-segment-up-to: no longer poke around in make-string buffer (now | Makarius Wenzel | |
| more efficient, also works around crash bug in xemacs-21.1.7/SuSE); | |||
| 2000-04-07 | More generic message to avoid confusion with Coq searching. | David Aspinall | |
| 2000-04-04 | Improved behaviour of electric terminator. | David Aspinall | |
| 2000-04-04 | Update copyright dates, comments. | David Aspinall | |
| 2000-03-24 | Spacing. | David Aspinall | |
| 2000-03-22 | Bug fix for electric terminator used inside locked region. | David Aspinall | |
| 2000-03-22 | Use proof-format-filename instead of format on cmds with file parameter. | David Aspinall | |
| 2000-03-19 | Added keybinding, improved doc for ↵ | David Aspinall | |
| proof-undo-and-delete-last-successful-command. | |||
| 2000-03-10 | Use name of proof assistant in menu. | David Aspinall | |
| 2000-02-09 | Added proof-shell-pre-interrupt-hook | David Aspinall | |
| 1999-11-24 | Docstring | David Aspinall | |
| 1999-11-24 | Fixed extending queue bug. Many docstring improvements | David Aspinall | |
| 1999-11-23 | Fixed bug introduced by hacking proof-only-whitespace-to-locked-region-p. | David Aspinall | |
| 1999-11-22 | Renamed proof-auto-delete-windows -> proof-delete-empty-windows | David Aspinall | |
| 1999-11-22 | Improved nothing to do error message | David Aspinall | |
| 1999-11-19 | Typo | David Aspinall | |
| 1999-11-19 | Fix for proof-script-new-command-advance. | David Aspinall | |
| 1999-11-18 | Removed comment. | David Aspinall | |
| 1999-11-18 | Changed eval-when-compile to eval-when (compile). | David Aspinall | |
| Made a new menu for quick options editing, put it in shared menu. Added options for multiple frames, auto delete windows. Toolbar :active is now more sringent, must be in script buffer. Use proof-try-require to load func-menu in mode definition, solving problem of func-menu configuration before it's loaded. Cleaned up some comments. | |||
| 1999-11-17 | Fix mouse bindings to be different for FSF/XEmacs versions. | David Aspinall | |
| 1999-11-17 | Fix typo | David Aspinall | |
| 1999-11-17 | Add Function Menu to menu. Fix a few bugs/probs shown up by byte-compiling. | David Aspinall | |
| 1999-11-16 | Not strictly necessary to set proof-goal-command-regexp | David Aspinall | |
| 1999-11-16 | Added proof-mouse-goto-point, moved proof-mouse-track-insert to proof-script | David Aspinall | |
| 1999-11-16 | Fix for proof-minibuffer-cmd. Remove old keybindings. | David Aspinall | |
| 1999-11-16 | Fix for retraction order with auto-multiple-files. | David Aspinall | |
| Let proof-undo-and-delete-last-successful-command work from other buffers. Made kill buffer function more robust. New! Added generic defaults for count-undos, goal-command-p, state-preserving-p. Used in demoisa instance for now, others to use later. Added checks that important configuration variables are set, and set defaults for some others. | |||
| 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). | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |