| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-16 | Docstrings, bug report msg. Added proof-warn-if-unset. | David Aspinall | |
| 1999-11-16 | Fix to shell filter for non-wakeup char instances of PG. | David Aspinall | |
| 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. | |||
| 1999-11-16 | New settings for generic count-undos code: | David Aspinall | |
| proof-non-undoables-regexp, proof-ignore-for-undo-count, Added proof-shell-quit-timeout Deprecate brand new setting proof-goals-display-qed-message. Improved docstrings, changed some defaults to useful values. | |||
| 1999-11-15 | Splash time=2, trying to unify FSF and XEmacs. | David Aspinall | |
| 1999-11-15 | docstring | David Aspinall | |
| 1999-11-15 | Repaired FSF font-locking. Define toggler for output hilite enable. | David Aspinall | |
| 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 | Set version tag for new release. | David Aspinall | |
| 1999-11-15 | Moved proof-switch-to-buffer here from proof-script.el | David Aspinall | |
| 1999-11-15 | Moved code for user-commands to proof-script.el. | David Aspinall | |
| 1999-11-15 | proof-grab-lock calls proof-shell-ready-prover with queuemode arg. ↵ | David Aspinall | |
| Docstring and debug msgs | |||
| 1999-11-15 | Reorganization of user-level commands, code moved from proof-toolbar.el | David Aspinall | |
| 1999-11-15 | Name changes: proof-toolbar-follow-mode -> proof-follow-mode, ↵ | David Aspinall | |
| proof-execute-minibuffer-cmd -> proof-minibuffer-cmd | |||
| 1999-11-15 | Some new macros. FSF fix for font-lock. Failed attempt not to turn on ↵ | David Aspinall | |
| font-lock everywhere. | |||
| 1999-11-15 | Cleanup and use some macros from proof.el | David Aspinall | |
| 1999-11-15 | FSF fix: require cl. | 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-15 | Added proof-splash-message. | David Aspinall | |
| 1999-11-15 | Fix for FSF Emacs. Added timeout arg to proof-shell-wait. | David Aspinall | |
| 1999-11-15 | Tuned splash screen for FSF emacs. Added proof-font-lock-zap-commas | David Aspinall | |
| 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 | docstring | David Aspinall | |
| 1999-11-14 | Fix to docstring magic (allow spaces after symbol). | David Aspinall | |
| 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-13 | comments | David Aspinall | |
| 1999-11-13 | Added example instantiation demoisa | David Aspinall | |
| 1999-11-13 | Added new face for debug messages | David Aspinall | |
| 1999-11-12 | Notes about font-lock management. | David Aspinall | |
| 1999-11-12 | Fixes for Isabelle in case theory file is visited before script file. | David Aspinall | |
| 1999-11-12 | Document variables before functions in case of name clash. | David Aspinall | |
| 1999-11-12 | Added ACTION to proof-shell-insert so proof-shell-insert-hook can test class ↵ | David Aspinall | |
| of command. (For Plastic) | |||
| 1999-11-12 | Made display table stuff interactive. | David Aspinall | |
| 1999-11-12 | Changed colour of proof-locked-face | David Aspinall | |
| 1999-11-12 | Fix for automode list | David Aspinall | |
| 1999-11-12 | Typo in x-symbol enable | David Aspinall | |
| 1999-11-12 | Typo in x-symbol enable | David Aspinall | |
| 1999-11-12 | Set version tag for new release. | David Aspinall | |
| 1999-11-12 | Fixes for response buffer display, x-symbol, output formatting. | David Aspinall | |
| 1999-11-11 | Attempted x-symbol improvements | David Aspinall | |
| 1999-11-11 | Added option for sending qed output to goals buffer for Isabelle | David Aspinall | |
| 1999-11-11 | small changes to plastic mode | Paul Callaghan | |
| 1999-11-11 | Removed debug instruction. | 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 | Patches for urgent message processing. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |