proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Made PROOF logo same width as GENERAL. Made both have transparent background.	David Aspinall	1998-11-18
\|
*	A few more	David Aspinall	1998-11-18
\|
*	Added NewDoc temporaries	David Aspinall	1998-11-18
\|
*	Improvements for multiple files. Now saves state specially for ProofGeneral.	David Aspinall	1998-11-18
\|
*	Added isa-update function. Altered settings.	David Aspinall	1998-11-18
\|
*	proof-done-retracting: changed delete-region to kill-region after	David Aspinall	1998-11-18
\| \| \| \|	Martin Hofmann's suggestion.
*	Bug fix: proof-undo-last-successful-command has silent failure for	David Aspinall	1998-11-18
\| \| \| \|	empty locked region.
*	proof-response-buffer-display: Move point to the end of the buffer	David Aspinall	1998-11-18
\| \| \| \|	after all. It can get moved by the display functions.
*	Changes for better testing	David Aspinall	1998-11-18
\|
*	Fixed problem with list_loaded_files and update().	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \|	Now when doing use_thy, we don't do an update. Hopefully "following children are out of date" message will be superfluous because they will be unlocked already. Will be re-read as needed. Added update function. Fixed up implementation of list_parents.
*	Added Proof General menu to theory file mode.	David Aspinall	1998-11-18
\|
*	. Changed behaviour of retracting current scripting buffer:	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \| \| \|	now it nukes proof-script-buffer-list (possibly unecessarily). Before, current scripting buffer was silently preserved in case it was retracted, but this means that proof-activate-scripting-hook was not run when scripting was begun again in the buffer, which left PG in an inconsistent state with respect to included files (in Isabelle). URGENT: must check this is okay with LEGO.
*	. Bug fix: moved proof-mark-buffer-atomic from proof-mode body to	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	proof-config-done, since it relies on some configuration being set! . Removed test for script buffer in proof-unprocessed-begin to allow non-script buffers to be properly recognized as being locked. . Proof restart script now works on all included files, not just those in the proof-script-buffer-list. This means non script buffers are correctly unlocked when scripting is restarted. . Bug fix in proof-register-possibly-new-processed-file to mark buffer atomic according to the comment (previously failed if proof-script-buffer-list happened to be empty) . Bug fix so proof-undo-last-successful-command fails silently on buffer without locked regions.
*	Improved proof-clean-buffer. Now only deletes windows in currently	David Aspinall	1998-11-18
\| \| \| \| \|	selected frame. Changed default proof-auto-delete-windows value back to t.
*	improvements to docstrings and defcustoms.	David Aspinall	1998-11-18
\| \| \| \|	added proof-shell-clear-response-regexp
*	Bug fix and adjustments in proof-response-buffer-display	David Aspinall	1998-11-18
\|
*	Removed proof-response-buffer-display from byte compile autoloads	David Aspinall	1998-11-18
\|
*	. bug fix for proof-shell-live-buffer.	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	. bug fix for proof-shell-filter for case that prompt isn't seen in first output chunk. . bug fix of handling urgent messages in delayed output: skip past the last one seen. Previously messages were put into the response buffer twice (first time highlighted). Don't clear the response buffer between urgent messages and delayed output within the same prompt-delimited region. . big improvement of display handling for response buffer, via new function proof-shell-maybe-erase-response. . added proof-shell-clear-response-regexp . docstring fixes.
*	Added optional argument to proof-ids for non-comma separators.	David Aspinall	1998-11-18
\|
*	Added clear_response_buffer regexp, use_thy_and_update now in ProofGeneral	David Aspinall	1998-11-18
\|
*	Improvements and cleanups:	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \|	. Put functions into ProofGeneral structure . Annotations around ordinary output appear before cr's . Added clear_response_buffer functionw . Added special_theories to avoid looking up filenames of theories which don't have them
*	Added notes of default values for user options.	David Aspinall	1998-11-18
\|
*	new file to factor out improved theory reader junk.	David Aspinall	1998-11-18
\|
*	Added section on theory files to Isabelle chapter	David Aspinall	1998-11-12
\|
*	Minor fixes/improvements	David Aspinall	1998-11-12
\|
*	Bug in regexp	David Aspinall	1998-11-12
\|
*	In a fit of autocracy, removed proof-tags-support, binding for	David Aspinall	1998-11-12
\| \| \| \| \| \|	M-tab and appearance of Find Tags in PG menu. The menu entry already appears in Tools->Tags, and users should bind M-tab for themselves.
*	More re-ordering to move important stuff up the list	David Aspinall	1998-11-12
\|
*	Added Goals buffer to buffers menu -- I forgot it\!	David Aspinall	1998-11-12
\|
*	Rashly fixed a suspicious looking nested use of set-buffer. Docstrings.	David Aspinall	1998-11-12
\|
*	Fixed error regexp	David Aspinall	1998-11-12
\|
*	Added "Changing faces" section.	David Aspinall	1998-11-12
\| \| \| \|	Added documentation for proof-auto-delete-windows.
*	Added proof-auto-delete-windows user option.	David Aspinall	1998-11-12
\|
*	Minor improvement to atrocious performance of proof-sement-up-to.	David Aspinall	1998-11-12
\|
*	Note about atrocious performance of proof-sement-up-to, even when compiled.	David Aspinall	1998-11-12
\|
*	Reorganized.	David Aspinall	1998-11-12
\|
*	Fixed a regexp.	David Aspinall	1998-11-12
\|
*	Fixed bug with find-next-terminator.	David Aspinall	1998-11-12
\|
*	Added note about removing proof-goal-command-p	David Aspinall	1998-11-12
\|
*	Added setting for proof-goal-command-regexp	David Aspinall	1998-11-12
\|
*	Renamed proof-mode-name -> proof-general-name.	David Aspinall	1998-11-12
\| \| \| \| \| \|	Reimplemented configuration for fume-menu. Now works for named goals, named saves, and (e.g. lego) both! Removed some FIXME's.
*	Replaced custom-set-variables with customize-set-variable:	David Aspinall	1998-11-12
\| \| \| \| \|	the first one sets the saved value for variables, rather than default values.
*	Removed some Emacs jargon from features list.	David Aspinall	1998-11-12
\|
*	Set version tag for new release.	David Aspinall	1998-11-10
\|
*	added entry to convert dvi into ps.	Thomas Kleymann	1998-11-10
\|
*	Added doc to short term improvements. It won't be good for 2.0, 8-(.	David Aspinall	1998-11-10
\|
*	Disabled problematic requires temporarily.	David Aspinall	1998-11-10
\|
*	Added buffers menu, and added shared menu to shell and response buffers.	David Aspinall	1998-11-10
\|
*	Added X idea for using indirect buffers.	David Aspinall	1998-11-10
\|
*	Removed references of proof-shell-noise-regexp	Thomas Kleymann	1998-11-10
\|