Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add sanity check on important settings for proof shell (underway) | 2000-09-12 | |
| | |||
* | Added proof-shell-auto-terminate-commands | 2000-08-29 | |
| | |||
* | Added proof-shell-set-elisp-variable-regexp | 2000-08-28 | |
| | |||
* | Added split string on theorem dependency code, to make list of dependents. | 2000-08-14 | |
| | |||
* | bug fixing in matching theorem dependencies | 2000-07-19 | |
| | |||
* | changes to add theorem dependencies recording in spans | 2000-07-19 | |
| | |||
* | Remove modeline from extra frames (in XEmacs). | 2000-06-22 | |
| | |||
* | Strange ? got in by accident. | 2000-06-09 | |
| | |||
* | Remove toolbar and menubar from windows in multiple frame mode. | 2000-06-09 | |
| | |||
* | Added proof-next-error. | 2000-06-05 | |
| | | | | | proof-shell-invisible-command: add terminator if it seems to be missing (after all: it's useful for users with C-c C-v). | ||
* | Use proof-running-on-XEmacs variable. | 2000-06-01 | |
| | |||
* | Made require on proof-menu instead of proof-script. | 2000-06-01 | |
| | |||
* | Change order of checks in proof-shell-live-buffer | 2000-05-30 | |
| | |||
* | Don\'t wait for ever if process dies on startup | 2000-05-29 | |
| | |||
* | Patch for synchronization problem in Coq, perhaps others. | 2000-05-25 | |
| | |||
* | Note abut ;;;###autoload not working for define-derived-mode. | 2000-05-11 | |
| | |||
* | Improved loading | 2000-05-09 | |
| | |||
* | Corrected header. | 2000-05-05 | |
| | |||
* | Comment. | 2000-04-07 | |
| | |||
* | pbp-mode -> goals-mode | 2000-04-07 | |
| | |||
* | Fixed up proof-shell-proof-completed mess nicely. | 2000-04-07 | |
| | |||
* | Added implementation of silent switch for turning on/off prover output. | 2000-04-04 | |
| | |||
* | Added proof-shell-clear-state function to collect together state clearing ops. | 2000-04-04 | |
| | |||
* | Update copyright dates, comments. | 2000-04-04 | |
| | |||
* | Fix for activating multiple frames when no active scripting buffer. | 2000-03-22 | |
| | |||
* | Comment | 2000-03-19 | |
| | |||
* | Comment about proof-goals-display-qed-message mess. | 2000-03-13 | |
| | |||
* | Names of shell, goals, script buffers now based on proof assistant name | 2000-03-10 | |
| | |||
* | Added proof-shell-process-connection-type. | 2000-03-09 | |
| | |||
* | Forced process-connection-type always to nil, after all. May not be an ↵ | 2000-02-29 | |
| | | | | issue with non-mule FSF Emacs (that was something different). | ||
* | Added back ^G fix for Solaris, but not for non-mule FSF. | 2000-02-28 | |
| | |||
* | Temporary fix for problem with Emacs 20.5 reported by Pierre | 2000-01-25 | |
| | |||
* | Typo | 1999-11-29 | |
| | |||
* | Comments about improved handling of urgent message markers, following | 1999-11-29 | |
| | | | | | | jrl's bug report about duplication of occasional urgent messages. The correct fix is to set proof-shell-eager-annotation-start-length properly. | ||
* | Moved proof-analyse-using-stack to proof-config. Added docstrings for pbp ↵ | 1999-11-24 | |
| | | | | functions. | ||
* | Don't bind button1 in goals buffer, so cut and paste still work. | 1999-11-23 | |
| | |||
* | proof-shell-done-invisible -> proof-done-invisible again | 1999-11-22 | |
| | |||
* | Added pbp-yank-subterm, changed mouse bindings for goals buffer. | 1999-11-19 | |
| | |||
* | Automatically generate special-display-regexps entry, and | 1999-11-18 | |
| | | | | | | | add function for new multiple frames user option. Don't display "done" in goals buffer (may never happen anyway) Remove code for response buffer erasing. Clean some comments. | ||
* | Bind mouse 2 as well as mouse 3 for pbp | 1999-11-17 | |
| | |||
* | Added some new code from another patch, but commented out for now. | 1999-11-17 | |
| | |||
* | Fix mouse bindings to be different for FSF/XEmacs versions. | 1999-11-17 | |
| | |||
* | Fix a few bugs/probs shown up by byte-compiling. | 1999-11-17 | |
| | |||
* | Strip CRs from minibuf messages for FSF's sake to remove ^Js. Attempt to ↵ | 1999-11-16 | |
| | | | | fix 'no-catch for exited tag' buglet. | ||
* | Added proof-mouse-goto-point, moved proof-mouse-track-insert to proof-script | 1999-11-16 | |
| | |||
* | Fix to shell filter for non-wakeup char instances of PG. | 1999-11-16 | |
| | | | | | | | | | | | 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. | ||
* | docstring | 1999-11-15 | |
| | |||
* | proof-grab-lock calls proof-shell-ready-prover with queuemode arg. ↵ | 1999-11-15 | |
| | | | | Docstring and debug msgs | ||
* | Fix for FSF Emacs. Added timeout arg to proof-shell-wait. | 1999-11-15 | |
| | |||
* | Many robustness improvements for error and interrupt handling: | 1999-11-14 | |
| | | | | | | | | | | | | - 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) |