proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Clarify require	David Aspinall	2009-09-08
\|
*	Require on scomint	David Aspinall	2009-09-08
\|
*	proof-shell-handle-error-output: renamed, and simplified	David Aspinall	2009-09-08
\| \| \| \| \|	to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup.
*	Fix docstrings, remove spurious null	David Aspinall	2009-09-08
\|
*	pg-response-display-with-face: remove update of `proof-shell-last-output'	David Aspinall	2009-09-08
\|
*	Remove use of regexp-opt-depth and clarify doc of	David Aspinall	2009-09-08
\| \| \| \| \|	`unicode-tokens-token-match-regexp'. Fix typo in `proof-tactical-name-face'.
*	Remove devel. from testall target	David Aspinall	2009-09-08
\|
*	Remove warnings in batch compile about functions possibly undefined at	David Aspinall	2009-09-08
\| \| \| \| \|	runtime. Most of these are spurious (come from autoloads; byte comp seems to give these higher priority than declarations in same file).
*	Only show splash message if noninteractive	David Aspinall	2009-09-07
\|
*	Remove load order tweak experiment	David Aspinall	2009-09-07
\|
*	Nuke spurious warning	David Aspinall	2009-09-07
\|
*	Update autoloads	David Aspinall	2009-09-07
\|
*	Fix proof-shell-trace-output-regexp: match on annotation \^AI now too	David Aspinall	2009-09-07
\|
*	Deleted file	David Aspinall	2009-09-07
\|
*	Require unicode-tokens during compile.	David Aspinall	2009-09-07
\|
*	scomint-check-proc: make defsubst	David Aspinall	2009-09-07
\|
*	Attempt to handle splash buffer cleanly.	David Aspinall	2009-09-07
\|
*	Revert change in 10.26 to use defpacustom after all, this gives	David Aspinall	2009-09-07
\| \| \| \| \|	the prover-specific menu entry automatically. Fix compiler warning with a defvar.
*	Fix initialisation of isar-use-find-theorems-form in compiled file.	David Aspinall	2009-09-07
\|
*	require proof-site also at startup	David Aspinall	2009-09-07
\|
*	lego-shell-process-output -> lego-shell-classify-output	David Aspinall	2009-09-07
\|
*	Requires processed more often (experiment)	David Aspinall	2009-09-07
\|
*	Fix compiler warnings	David Aspinall	2009-09-07
\|
*	isar-use-find-theorems-form: use defcustom, not defpacustom	David Aspinall	2009-09-07
\| \| \| \|	isar-keywords-name: fix custom group
*	Fix compiler warnings	David Aspinall	2009-09-07
\|
*	Fix compiler warnings.	David Aspinall	2009-09-07
\|
*	Isabelle->isabelle binary. Remove Isar homepage.	David Aspinall	2009-09-07
\|
*	Don't try to compile obsolete twelf Emacs code.	David Aspinall	2009-09-07
\|
*	Update for 4.0 and shorten.	David Aspinall	2009-09-07
\|
*	(C) date	David Aspinall	2009-09-07
\|
*	Fix compile warnings and ensure compiled code behaves as expected.	David Aspinall	2009-09-07
\|
*	Fix compile warning, rearrange docs	David Aspinall	2009-09-07
\|
*	Require cl for compilation. Rearrange docs.	David Aspinall	2009-09-07
\|
*	Attempt byte compilation only for emacs lisp!	David Aspinall	2009-09-07
\|
*	isar-preprocessing: remove unnecessary save-match-data.	David Aspinall	2009-09-07
\| \| \| \|	Fix a compile warning.
*	Remove \t in \<inverse> expansion.	David Aspinall	2009-09-07
\| \| \| \|	Make \<spacespace> be a single EM-DASH SPACE
*	Remove \t in \<module> expansion.	David Aspinall	2009-09-07
\|
*	Fix compile warnings	David Aspinall	2009-09-07
\|
*	Whitespace	David Aspinall	2009-09-07
\|
*	(C) date	David Aspinall	2009-09-07
\|
*	mapcar -> dolist	David Aspinall	2009-09-07
\|
*	Require cl for compilation	David Aspinall	2009-09-07
\|
*	Missing require	David Aspinall	2009-09-07
\|
*	Fix typos	David Aspinall	2009-09-07
\|
*	Update for Unicode Tokens.	David Aspinall	2009-09-07
\|
*	Add documentation to explain usage.	David Aspinall	2009-09-07
\| \| \| \| \|	Add setting function for dynamic updates. Add further symbols and explanation of two ways of working.
*	Use extended form of define-minor-mode	David Aspinall	2009-09-07
\|
*	Add template auto-insert hook	David Aspinall	2009-09-07
\|
*	Calculate token match regexp in a more complex way in an attempt to	David Aspinall	2009-09-07
\| \| \| \| \| \|	allow for Coq token grammar. Alter composition of strings to place characters by baseline. Doc and menu notes about replacement functions.
*	Updated	David Aspinall	2009-09-06
\|