aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
Commit message (Collapse)AuthorAge
* Call (proof-toolbar-setup) to add toolbar to goals and response bufferGravatar David Aspinall2000-09-23
| | | | Unify goals and response menus with script buffer menu
* Add sanity check on important settings for proof shell (underway)Gravatar David Aspinall2000-09-12
|
* Added proof-shell-auto-terminate-commandsGravatar David Aspinall2000-08-29
|
* Added proof-shell-set-elisp-variable-regexpGravatar David Aspinall2000-08-28
|
* Added split string on theorem dependency code, to make list of dependents.Gravatar David Aspinall2000-08-14
|
* bug fixing in matching theorem dependenciesGravatar David Aspinall2000-07-19
|
* changes to add theorem dependencies recording in spansGravatar David Aspinall2000-07-19
|
* Remove modeline from extra frames (in XEmacs).Gravatar David Aspinall2000-06-22
|
* Strange ? got in by accident.Gravatar David Aspinall2000-06-09
|
* Remove toolbar and menubar from windows in multiple frame mode.Gravatar David Aspinall2000-06-09
|
* Added proof-next-error.Gravatar David Aspinall2000-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.Gravatar David Aspinall2000-06-01
|
* Made require on proof-menu instead of proof-script.Gravatar David Aspinall2000-06-01
|
* Change order of checks in proof-shell-live-bufferGravatar David Aspinall2000-05-30
|
* Don\'t wait for ever if process dies on startupGravatar David Aspinall2000-05-29
|
* Patch for synchronization problem in Coq, perhaps others.Gravatar David Aspinall2000-05-25
|
* Note abut ;;;###autoload not working for define-derived-mode.Gravatar David Aspinall2000-05-11
|
* Improved loadingGravatar David Aspinall2000-05-09
|
* Corrected header.Gravatar David Aspinall2000-05-05
|
* Comment.Gravatar David Aspinall2000-04-07
|
* pbp-mode -> goals-modeGravatar David Aspinall2000-04-07
|
* Fixed up proof-shell-proof-completed mess nicely.Gravatar David Aspinall2000-04-07
|
* Added implementation of silent switch for turning on/off prover output.Gravatar David Aspinall2000-04-04
|
* Added proof-shell-clear-state function to collect together state clearing ops.Gravatar David Aspinall2000-04-04
|
* Update copyright dates, comments.Gravatar David Aspinall2000-04-04
|
* Fix for activating multiple frames when no active scripting buffer.Gravatar David Aspinall2000-03-22
|
* CommentGravatar David Aspinall2000-03-19
|
* Comment about proof-goals-display-qed-message mess.Gravatar David Aspinall2000-03-13
|
* Names of shell, goals, script buffers now based on proof assistant nameGravatar David Aspinall2000-03-10
|
* Added proof-shell-process-connection-type.Gravatar David Aspinall2000-03-09
|
* Forced process-connection-type always to nil, after all. May not be an ↵Gravatar David Aspinall2000-02-29
| | | | issue with non-mule FSF Emacs (that was something different).
* Added back ^G fix for Solaris, but not for non-mule FSF.Gravatar David Aspinall2000-02-28
|
* Temporary fix for problem with Emacs 20.5 reported by PierreGravatar David Aspinall2000-01-25
|
* TypoGravatar David Aspinall1999-11-29
|
* Comments about improved handling of urgent message markers, followingGravatar David Aspinall1999-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 ↵Gravatar David Aspinall1999-11-24
| | | | functions.
* Don't bind button1 in goals buffer, so cut and paste still work.Gravatar David Aspinall1999-11-23
|
* proof-shell-done-invisible -> proof-done-invisible againGravatar David Aspinall1999-11-22
|
* Added pbp-yank-subterm, changed mouse bindings for goals buffer.Gravatar David Aspinall1999-11-19
|
* Automatically generate special-display-regexps entry, andGravatar David Aspinall1999-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 pbpGravatar David Aspinall1999-11-17
|
* Added some new code from another patch, but commented out for now.Gravatar David Aspinall1999-11-17
|
* Fix mouse bindings to be different for FSF/XEmacs versions.Gravatar David Aspinall1999-11-17
|
* Fix a few bugs/probs shown up by byte-compiling.Gravatar David Aspinall1999-11-17
|
* Strip CRs from minibuf messages for FSF's sake to remove ^Js. Attempt to ↵Gravatar David Aspinall1999-11-16
| | | | fix 'no-catch for exited tag' buglet.
* Added proof-mouse-goto-point, moved proof-mouse-track-insert to proof-scriptGravatar David Aspinall1999-11-16
|
* Fix to shell filter for non-wakeup char instances of PG.Gravatar David Aspinall1999-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.
* docstringGravatar David Aspinall1999-11-15
|
* proof-grab-lock calls proof-shell-ready-prover with queuemode arg. ↵Gravatar David Aspinall1999-11-15
| | | | Docstring and debug msgs
* Fix for FSF Emacs. Added timeout arg to proof-shell-wait.Gravatar David Aspinall1999-11-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:31:46 +0000