proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2006-12-05	Use Isar-specific isabelle-system file	David Aspinall

2006-11-07	Set version tag for new release.	David Aspinall

2006-11-04	isar-keywords-theory-enclose: removed isar-keywords-theory-switch, which ↵	Makarius Wenzel
	usually appears locally as plain theory command; isar-keywords-proper: simplified font-lock; added isar-match-nesting -- distinguishes font-lock for local vs. global begin/end;
2006-11-04	isar-strip-terminators, isar-detect-begin: proof-search-forward;	Makarius Wenzel

2006-10-29	New files.	David Aspinall

2006-10-29	Updated.	David Aspinall

2006-10-27	Set version tag for new release.	David Aspinall

2006-10-27	Rationalise testing for different values of window-system, to/and support ↵	David Aspinall
	more Emacs ports easily
2006-10-23	Error highlighting in coq only when scripting (not when sending	Pierre Courtieu
	command invisibly).
2006-10-11	reintroduced pg-subterm-first-special-char, which makes PG strip goal markup;	Makarius Wenzel
	isar-find-and-forget: no special treatment of undo-kill, allows "context" command to act as local theory init;
2006-10-11	isar-keywords-indent-enclose: include "begin" keyword;	Makarius Wenzel
	removed obsolete kill/undo-kill-regexp;
2006-10-11	added regexps for begin/end and theory start;	Makarius Wenzel

2006-10-11	removed obsolete isar-detect-header;	Makarius Wenzel
	isar-find-and-forget: proper handling of nested begin/end blocks;
2006-10-06	Fix for coq-utf-safe.	Pierre Courtieu

2006-09-29	utf safe coq mode is not linked to proof-shell-unicode, as unicode is	Pierre Courtieu
	not well handle by xemacs.
2006-09-29	adapting to proof-shell-unicode. Coq has not been adapted to the	Pierre Courtieu
	-emacs-U option.
2006-09-29	Simplified prompt regexp for coq, preparing new prompt delimiters	Pierre Courtieu
	<prompt> and </prompt>.
2006-09-29	fixed a bug with wakeup char for coq.	Pierre Courtieu

2006-09-25	Added \x6 as a possible wakeup char for coq. For the moment this	Pierre Courtieu
	special char is used when the -emacs-U is used (with or instead of -emacs) in cvs version of coq of today 25/9/2006.
2006-09-24	Set version tag for new release.	David Aspinall

2006-09-24	Tweaks to buffer history mode. Still intermediate version.	David Aspinall

2006-09-24	Deleted file	David Aspinall

2006-09-24	Add buffer history browsing	David Aspinall

2006-09-22	Fix typo.	David Aspinall

2006-09-22	Cut comint input ring, minor efficiency tweak.	David Aspinall

2006-09-22	Updated.	David Aspinall

2006-09-22	Tweak.	David Aspinall

2006-09-22	Fix typo.	David Aspinall

2006-09-22	Comments.	David Aspinall

2006-09-22	Add workaround for GNU Emacs problems in easymenu-add.	David Aspinall

2006-09-22	Update to 0.4.8 from sourceforge.	David Aspinall

2006-09-22	Set version tag for new release.	David Aspinall

2006-09-22	Packaging fixes: put isar/interface in right place; install examples and doc ↵	David Aspinall
	files from Makefile.
2006-09-22	Updated.	David Aspinall

2006-09-22	Deleted file	David Aspinall

2006-09-15	typo in coq-indent.	Pierre Courtieu

2006-09-15	fixed a typo in last correction.	Pierre Courtieu

2006-09-14	fix a bug with error highlighting. Not sure it is ok but seems to	Pierre Courtieu
	work.
2006-09-14	fixed a bug from Stefan Monnier.	Pierre Courtieu

2006-09-13	cleaning from Stefan Monnier.	Pierre Courtieu

2006-09-13	cleaning from Stefan Monnier.	Pierre Courtieu

2006-09-12	Updated.	David Aspinall

2006-09-12	Set version tag for new release.	David Aspinall

2006-09-09	Set version tag for new release.	David Aspinall

2006-09-08	Fixed nested comment support for scripting, in xemacs (worked already	Pierre Courtieu
	on GNU Emacs). Instanciated proof-parse-function for that...
2006-09-07	Set version tag for new release.	David Aspinall

2006-09-07	Updated.	David Aspinall

2006-09-07	update CHANGES.	Pierre Courtieu

2006-09-07	Updated CHANGES.	Pierre Courtieu

2006-09-07	Added Goal as a goal starter in syntax db.	Pierre Courtieu