aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Collapse)Author
1999-11-17Fix a few bugs/probs shown up by byte-compiling.David Aspinall
1999-11-17Add Function Menu to menu. Fix a few bugs/probs shown up by byte-compiling.David Aspinall
1999-11-16Strip CRs from minibuf messages for FSF's sake to remove ^Js. Attempt to ↵David Aspinall
fix 'no-catch for exited tag' buglet.
1999-11-16Not strictly necessary to set proof-goal-command-regexpDavid Aspinall
1999-11-16Second version of easy-config, without defvaralias use.David Aspinall
1999-11-16Fix type of proof-completed-proof-behaviour.David Aspinall
1999-11-16Working version of easy-config.David Aspinall
1999-11-16Turn debug messages off by default.David Aspinall
1999-11-16Added proof-mouse-goto-point, moved proof-mouse-track-insert to proof-scriptDavid Aspinall
1999-11-16Set version tag for new release.David Aspinall
1999-11-16Fix for proof-minibuffer-cmd. Remove old keybindings.David Aspinall
1999-11-16Note about how to use demoisa and isar instances. Other commentsDavid Aspinall
1999-11-16Added proof-string-match-safe and proof-stringfn-match (also safe)David Aspinall
1999-11-16Preliminary, not for 3.0.David Aspinall
1999-11-16Fix 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-16Docstrings, bug report msg. Added proof-warn-if-unset.David Aspinall
1999-11-16Fix 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-16New 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-15Splash time=2, trying to unify FSF and XEmacs.David Aspinall
1999-11-15docstringDavid Aspinall
1999-11-15Repaired FSF font-locking. Define toggler for output hilite enable.David Aspinall
1999-11-15Fixed mistake in function names. Tidied menus a bitDavid Aspinall
1999-11-15Fixes for FSF overlay obscurity.David Aspinall
1999-11-15Set version tag for new release.David Aspinall
1999-11-15Moved proof-switch-to-buffer here from proof-script.elDavid Aspinall
1999-11-15Moved code for user-commands to proof-script.el.David Aspinall
1999-11-15proof-grab-lock calls proof-shell-ready-prover with queuemode arg. ↵David Aspinall
Docstring and debug msgs
1999-11-15Reorganization of user-level commands, code moved from proof-toolbar.elDavid Aspinall
1999-11-15Name changes: proof-toolbar-follow-mode -> proof-follow-mode, ↵David Aspinall
proof-execute-minibuffer-cmd -> proof-minibuffer-cmd
1999-11-15Some new macros. FSF fix for font-lock. Failed attempt not to turn on ↵David Aspinall
font-lock everywhere.
1999-11-15Cleanup and use some macros from proof.elDavid Aspinall
1999-11-15FSF fix: require cl.David Aspinall
1999-11-15Reorganization 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-15Added proof-splash-message.David Aspinall
1999-11-15Fix for FSF Emacs. Added timeout arg to proof-shell-wait.David Aspinall
1999-11-15Tuned splash screen for FSF emacs. Added proof-font-lock-zap-commasDavid Aspinall
1999-11-14Fixes for proof-goto-commmand-{end,start}. Former new functionDavid Aspinall
1999-11-14Many 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-14docstringDavid Aspinall
1999-11-14Fix to docstring magic (allow spaces after symbol).David Aspinall
1999-11-14proof-nested-goals-allowed -> proof-completed-proof-behaviourDavid Aspinall
Patch for more flexible handling of closing goal...save regions after proof has been completed.
1999-11-13Beginnings of improved version of goal..no save regions.David Aspinall
1999-11-13commentsDavid Aspinall
1999-11-13Added example instantiation demoisaDavid Aspinall
1999-11-13Added new face for debug messagesDavid Aspinall
1999-11-12Notes about font-lock management.David Aspinall
1999-11-12Fixes for Isabelle in case theory file is visited before script file.David Aspinall
1999-11-12Document variables before functions in case of name clash.David Aspinall
1999-11-12Added ACTION to proof-shell-insert so proof-shell-insert-hook can test class ↵David Aspinall
of command. (For Plastic)
1999-11-12Made display table stuff interactive.David Aspinall