proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Harmonise a bit more with X-Symbols. Add customization facility	David Aspinall	2008-01-30
\|
*	isar-undos: fix bug trac #189 introduced by attempt to remove proof-no-command.	David Aspinall	2008-01-29
\|
*	Set proof-shell-trace-output-regexp early enough to have effect. Fixes trac ↵	David Aspinall	2008-01-29
\| \| \| \|	#183, #186. See #190
*	Switch to fake long symbols	David Aspinall	2008-01-28
\|
*	Prevent prompt during compilation	David Aspinall	2008-01-28
\|
*	Add hooks for unicode tokens within proof shell	David Aspinall	2008-01-28
\|
*	Add shortcuts for tokens.	David Aspinall	2008-01-28
\|
*	Switch token table mapping destination from glyph names to unicode strings. ↵	David Aspinall	2008-01-27
\| \| \| \|	Generate from Isabelle.sym
*	fixed usage: default for option -p is emacs, not xemacs;	Makarius Wenzel	2008-01-25
\|
*	Fix previous change.	David Aspinall	2008-01-25
\|
*	Make isatool usage (view doc) compatible with proof-rsh-command.	David Aspinall	2008-01-25
\|
*	Make isatool usage compatible with proof-rsh-command.	David Aspinall	2008-01-25
\|
*	New files.	David Aspinall	2008-01-25
\|
*	Remove use of proof-ass	David Aspinall	2008-01-24
\|
*	Add key binding for ML {* *} and fix longsuper, longsub	David Aspinall	2008-01-24
\|
*	Updated.	David Aspinall	2008-01-16
\|
*	Updated.	David Aspinall	2008-01-16
\|
*	Default to using emacs now	David Aspinall	2008-01-15
\|
*	Many compatibility updates, bug fixes, rearrangements for compilation.	David Aspinall	2008-01-15
\|
*	Move x-symbol-isabelle -> x-symbol-isar to simplify setup.	David Aspinall	2007-12-14
\|
*	Deleted file	David Aspinall	2007-12-14
\|
*	Typo in pg-special-char-regexp	David Aspinall	2007-12-14
\|
*	x-symbol-isabelle-prepare-table: specialise to Isar (usefully removes ↵	David Aspinall	2007-12-14
\| \| \| \|	dependence on proof-assistant-symbol)
*	Remove eval-when, seems unreliable	David Aspinall	2007-12-14
\|
*	Improve loading; these tests are not functioning yet	David Aspinall	2007-12-14
\|
*	Make value of pg-special-char-regexp depend on proof-shell-unicode.	David Aspinall	2007-12-14
\| \| \| \|	This makes sure that stripping special characters from output is accurate.
*	Cleanup. Add more insertion commands.	David Aspinall	2007-12-13
\|
*	Deleted file	David Aspinall	2007-12-13
\|
*	Comment unused function	David Aspinall	2007-12-09
\|
*	clarify that -U now defaults to true;	Makarius Wenzel	2007-11-20
\|
*	command 'thm' makes no sense outside a proper context;	Makarius Wenzel	2007-11-13
\| \| \| \|	fixed spelling;
*	Versions	David Aspinall	2007-11-12
\|
*	proof-shell-issue-pgip-cmd is always isabelle-process-pgip;	Makarius Wenzel	2007-10-24
\|
*	removed obsolete isabelle-version-string, isa-version, isa-supports-pgip;	Makarius Wenzel	2007-10-24
\|
*	isar-find-and-forget: no special treatment of begin/end, just plain undo	Makarius Wenzel	2007-10-18
\| \| \| \|	(in Isabelle2005 this will produce repeated errors after end-of-theory;
*	isar-undo-fail-regexp: only isar-keywords-control, not isar-keywords-theory-end;	Makarius Wenzel	2007-10-18
\|
*	allow more specials: oct 327 .. oct 340;	Makarius Wenzel	2007-09-07
\|
*	isar-output-font-lock-keywords-1: hilite markup uses proof-warning-face;	Makarius Wenzel	2007-09-07
\|
*	pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing ↵	David Aspinall	2007-08-19
\| \| \| \|	markup (special 377).
*	removed outated comment;	Makarius Wenzel	2007-08-15
\|
*	isar-goalhyplit-test: explicit end-marker;	Makarius Wenzel	2007-08-15
\|
*	Add support for sending back literal commands reusing PBP markup mechanisms.	David Aspinall	2007-08-14
\|
*	isar-improper-regexp: include "prems";	Makarius Wenzel	2007-06-14
\| \| \| \|	Cvs: ----------------------------------------------------------------------
*	single-char-regexp: tuned symbol regexp;	Makarius Wenzel	2007-06-14
\| \| \| \|	subscript-matcher: more robust handling of non-space lookahead (beware of markuo specials!);
*	isar-font-lock-local: tuned symbol regexp;	Makarius Wenzel	2007-06-14
\|
*	reverted find theorems default from form to minibuffer	weber	2007-06-11
\|
*	XEmacs 21.4.15 does not seem to know propertize	weber	2007-05-17
\|
*	Fix rename	weber	2007-05-11
\|
*	Fix rename	weber	2007-05-11
\|
*	works with XEmacs now (ticket #115)	weber	2007-05-11
\|