| 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 | Fully working Isabelle PG in 30 setqs | David Aspinall | |
| 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-16 | Test files for automatic multiple files. | David Aspinall | |
| 1999-11-16 | Spruced up features list | David Aspinall | |
| 1999-11-15 | Splash time=2, trying to unify FSF and XEmacs. | David Aspinall | |
| 1999-11-15 | Updated | 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 | Remove xi, appears in exists. | David Aspinall | |
| 1999-11-15 | Set version tag for new release. | David Aspinall | |
| 1999-11-15 | -f to make rm quiet if no args. | David Aspinall | |
| 1999-11-15 | Updated | 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 | Change name of proof-execute-minibufer-cmd. | David Aspinall | |
| 1999-11-15 | Updated | David Aspinall | |
| 1999-11-15 | Use infixes to show off X-Symbol | David Aspinall | |
| 1999-11-15 | Added some greek letters. A mess if they occur in words. | David Aspinall | |
| 1999-11-15 | preliminary X-Symbol support | David Aspinall | |
| 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 | proof-font-lock-zap-commas=t | David Aspinall | |
| 1999-11-15 | Updated for new keybindings and menu layout. | David Aspinall | |
| 1999-11-15 | Removed proof-try-command. | 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 | Added in-testing message | David Aspinall | |
| 1999-11-15 | Removed font-lock settings. Set proof-font-lock-zap-commas=t | David Aspinall | |
| 1999-11-15 | Updated | 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 | More highlighting | David Aspinall | |
| 1999-11-14 | Updated | David Aspinall | |
| 1999-11-14 | devel.clean : use find to clean all subdirs. | 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-14 | Add demoisa dir to makefiles. | David Aspinall | |
| 1999-11-13 | Beginnings of improved version of goal..no save regions. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |