proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2011-09-19	Several improvements:	David Aspinall
	- explain how to use prefix commands for electric terminator as well as C-q - update explanation of locked region and read only options - explain colouring of modeline Scripting indicator - improve document-centred explanation, giving short-cut commands first - correct several uses of main menu "Proof General" to "Proof-General" with hyphen
2011-09-18	proof-full-annotation: default to nil	David Aspinall

2011-09-17	brute-force method to enable tool-bar-mode, which is especially important on ↵	Makarius Wenzel
	GNU Emacs for Mac OS X (change was already present in Isabelle2011);
2011-09-16	Set version tag for new release.	David Aspinall

2011-09-16	Tweak to Emacs package building	David Aspinall

2011-09-15	fix widget descriptions of coq-load-path	Hendrik Tews

2011-09-15	-add support for -R and -I -as in coq-load-path	Hendrik Tews
	-improve documentation (and reorder stuff)
2011-09-14	fix #421 with solution 1	Hendrik Tews

2011-09-14	proof-electric-terminator: allow a prefix argument to avoid electric action.	David Aspinall
	Addresses Trac #422
2011-09-14	# User Robin Green <greenrd@greenrd.org>	David Aspinall
	Use correct customisation widget for variable-length list of strings
2011-09-14	Fix typo	David Aspinall

2011-09-14	Remove contentious call to set-process-query-on-exit-flag, ref Trac#424	David Aspinall

2011-09-14	Add another contributor.	David Aspinall

2011-09-11	Fix proof-shell-exit optional argument with (interactive) thanks to	Pierre Courtieu
	Erik Martin-Dorel.
2011-09-09	fix documentation error	Hendrik Tews

2011-09-04	Fix trac #420 indentation freezing.	Pierre Courtieu

2011-09-04	some local buffer properties;	Makarius Wenzel

2011-08-31	Add suggestion for Q2 from Esben Andreasen to check comint-process-echoes.	David Aspinall

2011-08-31	clarified isar-improper-regexp -- "prems" is already reported as legacy by ↵	Makarius Wenzel
	the prover (after Isabelle2011);
2011-08-29	Non Unicode char	David Aspinall

2011-08-24	Capitalize menu items	David Aspinall

2011-08-24	Set version tag for new release.	David Aspinall

2011-08-24	eval-when-compile -> eval-when (compile) to avoid defvar coq-prog-name	David Aspinall
	overriding setting in coq.el
2011-08-23	Remove PG prefix from toolbar button names (needed for disambiguity in older ↵	David Aspinall
	Emacsen, displayed in Emacs 24 UI)
2011-08-23	Add back annotation for docstring for texinfo	David Aspinall

2011-08-23	Update magic	David Aspinall

2011-08-23	Set version tag for new release.	David Aspinall

2011-08-23	Note TODO for indent testing!	David Aspinall

2011-08-23	Move coq-prog-name back to coq.el	David Aspinall

2011-08-23	Crude patch for Trac #416. I haven't tried to understand indent code fully, ↵	David Aspinall
	so may not be best fix.
2011-07-29	Fixing track 414 by adding Preterm as a state preserving command.	Pierre Courtieu

2011-07-26	Updated.	David Aspinall

2011-07-26	Fix compile when smie isnt available	David Aspinall

2011-07-08	Fixing the scripting of new subproof script parenthesizing ({ and }).	Pierre Courtieu

2011-07-06	generalized font-lock regexps: isar-text allows any non-control characters ↵	Makarius Wenzel
	to be marked up (e.g. notation for "free" and "skolem" variables after Isabelle2011);
2011-07-05	+ fix documentation and one spelling error	Hendrik Tews

2011-07-01	Some more sample indentation patterns added.	Pierre Courtieu

2011-06-22	coq-use-smie not enabled by default	David Aspinall

2011-06-22	Remove pointer to closed ticket	David Aspinall

2011-06-22	Set version tag for new release.	David Aspinall

2011-06-22	Set version tag for new release.	David Aspinall

2011-06-19	Removed { and } as command terminators for now.	Pierre Courtieu
	Fixes #412.
2011-06-17	oops, undo last commit.	Pierre Courtieu

2011-06-17	Fix mais le find-father ne marche pas encore.	Pierre Courtieu

2011-06-11	* coq.el: Fix up a few comment conventions; Improve SMIE indentation.	Stefan Monnier
	(coq-smie-grammar): Use new special token "Proof End". (coq-smie-proof-end-tokens): New var. (coq-smie-forward-token, coq-smie-backward-token): Map proof end tokens to "Proof End", and map "(Next )Obligation" to "Proof". (coq-smie-rules): Indent after ;-tactical. Use "Proof End". Indent specially "Lemma x :forall, ..".
2011-06-10	Version bump	David Aspinall

2011-06-10	Set version tag for new release.	David Aspinall

2011-06-10	* empty log message *	David Aspinall

2011-06-10	Set version tag for new release.	David Aspinall

2011-06-10	Unplug smie cindentation code for this release.	Pierre Courtieu