proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	docstring	David Aspinall	1999-11-19
\|
*	Removed spurious defn of proof-config.el	David Aspinall	1999-11-19
\|
*	Added user option for multiple frames.	David Aspinall	1999-11-18
\|
*	Name change proof-window-dedicated -> proof-dont-switch-windows.	David Aspinall	1999-11-17
\|
*	Fix type of proof-completed-proof-behaviour.	David Aspinall	1999-11-16
\|
*	Turn debug messages off by default.	David Aspinall	1999-11-16
\|
*	New settings for generic count-undos code:	David Aspinall	1999-11-16
\| \| \| \| \| \| \| \|	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.
*	Splash time=2, trying to unify FSF and XEmacs.	David Aspinall	1999-11-15
\|
*	Name changes: proof-toolbar-follow-mode -> proof-follow-mode, ↵	David Aspinall	1999-11-15
\| \| \| \|	proof-execute-minibuffer-cmd -> proof-minibuffer-cmd
*	Tuned splash screen for FSF emacs. Added proof-font-lock-zap-commas	David Aspinall	1999-11-15
\|
*	Many robustness improvements for error and interrupt handling:	David Aspinall	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)
*	proof-nested-goals-allowed -> proof-completed-proof-behaviour	David Aspinall	1999-11-14
\| \| \| \| \|	Patch for more flexible handling of closing goal...save regions after proof has been completed.
*	Added new face for debug messages	David Aspinall	1999-11-13
\|
*	Added ACTION to proof-shell-insert so proof-shell-insert-hook can test class ↵	David Aspinall	1999-11-12
\| \| \| \|	of command. (For Plastic)
*	Changed colour of proof-locked-face	David Aspinall	1999-11-12
\|
*	Added option for sending qed output to goals buffer for Isabelle	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
\|
*	Reorganized user options. Special new code for boolean settings.	David Aspinall	1999-11-10
\|
*	Arrange for activate-scripting to not block for interactive calls.	David Aspinall	1999-11-09
\|
*	docstring	David Aspinall	1999-11-08
\|
*	proof-prf-string -> proof-showproof-command	David Aspinall	1999-11-08
\|
*	New section for x-symbol. New custom group for user options.	David Aspinall	1999-11-08
\|
*	Added proof-auto-multiple-files. Docstring addition.	David Aspinall	1999-10-25
\|
*	Added symmetric proof-shell-inform-file-retracted-cmd setting to correspond	David Aspinall	1999-10-21
\| \| \| \| \|	with the state change of a buffer from completely processed to partly processed.
*	Changed name of proof-shell-cd-cmd for uniformity.	David Aspinall	1999-10-21
\|
*	Changed name to proof-shell-inform-file-processed-cmd	David Aspinall	1999-10-21
\|
*	Added proof-shell-inform-file-processed-command setting.	David Aspinall	1999-10-21
\|
*	Docstring improvements	David Aspinall	1999-10-15
\|
*	Added message for reporting problems to splash screen.	David Aspinall	1999-10-12
\|
*	docstring magic	David Aspinall	1999-10-12
\|
*	docstring improved	David Aspinall	1999-10-12
\|
*	Added proof-toolbar-use-enablers.	David Aspinall	1999-10-12
\| \| \| \| \|	Set some defaults to nil to get sensible error messages instead of failure in Coq.
*	Speed optimizations, part I.	David Aspinall	1999-10-06
\|
*	More improvements/fixes for closing unfinished proofs.	David Aspinall	1999-10-06
\| \| \| \|	Added proof-unnamed-theorem-name.
*	docstring improvements	David Aspinall	1999-10-06
\|
*	Fixed coalescing of error messages: all error messages from	David Aspinall	1999-10-06
\| \| \| \|	the last command are now show. Added extra docs to clarify behaviour.
*	Docstrings. Added proof-nested-goals-allowed.	David Aspinall	1999-10-06
\|
*	Typo	David Aspinall	1999-10-06
\|
*	settings for (de)activating scripting, and proof-tidy-response.	David Aspinall	1999-10-06
\|
*	proof-try-command is deprecated	David Aspinall	1999-10-06
\|
*	Added proof-retract-buffer symmetric to proof-process-buffer.	David Aspinall	1999-10-06
\| \| \| \| \| \|	Added question to user when switching scripting buffer, and new option proof-auto-retract-other-buffers to disable question. This reimplements the old "steal scripting?" idea.
*	Fixup name changes	David Aspinall	1999-10-01
\|
*	Renamed some configuration variables for uniformity, see CHANGES.	David Aspinall	1999-10-01
\|
*	Unhappily added proof-shell-leave-annotations-in-output hack.	David Aspinall	1999-09-29
\|
*	Added proof-script-command-separator. Needs work.	David Aspinall	1999-09-29
\|
*	Docstrings	David Aspinall	1999-09-23
\|
*	Added proof-find-theorems-command setting.	David Aspinall	1999-09-23
\|
*	Docstrings	David Aspinall	1999-09-22
\|
*	proof-completed-regexp: match number 1 is response text;	Makarius Wenzel	1999-09-22
\|