proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
\|
*	(briefly) documented problem with sections in Coq	Thomas Kleymann	1998-11-10
\|
*	documented problem with Discharge in LEGO	Thomas Kleymann	1998-11-10
\|
*	Fixed bug for when proof-rsh-command is empty	David Aspinall	1998-11-10
\|
*	Changed text ready for 2.0 release	David Aspinall	1998-11-10
\|
*	Removed spurious fi	David Aspinall	1998-11-10
\|
*	Added some support for making a full release. Must edit html by hand though.	David Aspinall	1998-11-10
\|
*	Refresh response buffer when goals buffer is refreshed.	Thomas Kleymann	1998-11-10
\|
*	Fixes for byte compilations and missing bits of Isamode.	David Aspinall	1998-11-10
\|
*	Removed traces of support for Ruy's legogrep. This is superseded by legotags.	Thomas Kleymann	1998-11-10
\|
*	introduced section for FSF Emacs	Thomas Kleymann	1998-11-10
\|
*	Removed superfluous variable. Improved docstrings.	David Aspinall	1998-11-09
\|
*	Added docstring	David Aspinall	1998-11-09
\|
*	Updated user-view of our todo	David Aspinall	1998-11-09
\|
*	More reorganization. Added content to Isabelle chapter, begun basic script.	David Aspinall	1998-11-09
\|
*	Added proof-rsh-command to help complete documentation (was allocated	David Aspinall	1998-11-09
\| \| \| \|	to tms but he said he wouldn't get around to it)
*	Added bug about FSFmacs/proof-strict-read-only=t/font-lock	David Aspinall	1998-11-09
\|
*	Added proof-script-indent user option, to enable indentation code.	David Aspinall	1998-11-09
\| \| \| \| \| \|	Disabled by default. May be activated by particular proof assistants if they feel confident about it. I don't. Made proof-indent be autoloaded as needed. Lets pray it won't be.
*	Added section on multiple files	Thomas Kleymann	1998-11-09
\|
*	Added section on Isabelle specific bugs.	David Aspinall	1998-11-09
\|
*	Reduced a priority. Added release todo	David Aspinall	1998-11-09
\|