proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Note complete	David Aspinall	2010-08-08
\|
*	Checkdoc cleanups	David Aspinall	2010-08-08
\|
*	isabelle-string-face: introduce custom string colour as font lock default is ↵	David Aspinall	2010-08-04
\| \| \| \|	terrible
*	Swap phi and varphi for better consistency with STIX.	David Aspinall	2010-08-04
\|
*	isar-remove-file: remove (tail) recursion, leads to stack overflow	David Aspinall	2010-08-04
\|
*	proof-allow-undo-in-read-only: remove, use proof-strict-read-only instead.	David Aspinall	2010-08-03
\|
*	pg-protected-undo change	David Aspinall	2010-08-03
\|
*	pg-protected-undo: remove separate `proof-allow-undo-in-read-only' and	David Aspinall	2010-08-03
\| \| \| \| \|	make consistent with `proof-strict-read-only' setting. In particular, if "Edit Freely" is selected then we don't do any retraction.
*	proof-assert-electric-terminator: fix logic for inserting at buffer end	David Aspinall	2010-08-03
\|
*	Separate profiling from testing	David Aspinall	2010-08-03
\|
*	Simplify messaging code. Make sure random jumps do something. Fix ↵	David Aspinall	2010-08-03
\| \| \| \|	assert-processed to wait for shell.
*	Improve printing of test parameters.	David Aspinall	2010-08-03
\| \| \| \|	Add `pg-autotest-test-assert-full' for current buffer w/o file.
*	Show test log in case of failure	David Aspinall	2010-08-03
\|
*	Fix compile	David Aspinall	2010-08-03
\|
*	Temporarily disable splash	David Aspinall	2010-08-03
\|
*	Fix compilation	David Aspinall	2010-08-03
\|
*	Move key binding for proof assistant keymap (fixes compilation bug)	David Aspinall	2010-08-03
\|
*	Update	David Aspinall	2010-08-03
\|
*	Fix compile	David Aspinall	2010-08-03
\|
*	Resurrect autotest framework	David Aspinall	2010-08-03
\|
*	save-some-buffers: only offer to save proof script buffers	David Aspinall	2010-08-03
\|
*	proof-shell-wait, proof-shell-kill-function: avoid use of sit-for.	David Aspinall	2010-08-03
\|
*	less surprising unicode tokens: <-> corresponds to longleftrightarrow in ↵	Makarius Wenzel	2010-08-03
\| \| \| \|	common Isabelle theories (according to symbol length not shape), emdash is not predefined by default and confuses typical LaTeX source;
*	proof-deftoggle-fn: make ARG optional as suggested by docstring	David Aspinall	2010-08-03
\|
*	Updated.	David Aspinall	2010-08-03
\|
*	span-mapcar-spans-inorder: added for pg-movie production	David Aspinall	2010-08-03
\|
*	Fix theory name	David Aspinall	2010-08-03
\|
*	Support files for Movie output	David Aspinall	2010-08-03
\|
*	Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.	David Aspinall	2010-08-03
\|
*	Updated.	David Aspinall	2010-08-03
\|
*	Bump date (again)	David Aspinall	2010-08-03
\|
*	proof-full-annotation: default to t; advanced users may turn off.	David Aspinall	2010-08-03
\|
*	Move distribution examples into subdir	David Aspinall	2010-08-03
\|
*	Fix theory name	David Aspinall	2010-08-03
\|
*	Deleted file	David Aspinall	2010-08-03
\|
*	Fix for matching names in regexps, restores behaviour of name-aware code ↵	David Aspinall	2010-08-02
\| \| \| \|	such as imenu.
*	Add pg-protected-undo improved version due to Erik Martin-Dorel	David Aspinall	2010-08-02
\|
*	Update years, versions.	David Aspinall	2010-07-08
\|
*	Set version tag for new release.	David Aspinall	2010-07-08
\|
*	Cleanups for save-excursion to avoid warnings in latest Emacs versions	David Aspinall	2010-07-08
\|
*	save-excursion -> with-temp-buffer	David Aspinall	2010-07-08
\|
*	Replace uses of save-excursion with with-current-buffer. This	David Aspinall	2010-07-01
\| \| \| \| \|	prevents a spurious warning from Emacs 23 (and is a minor efficiency improvement).
*	plastic-shell-adjust-line-width: save-excursion -> with-current-buffer to avoid	David Aspinall	2010-07-01
\| \| \| \|	spurious warning in Emacs 23.2
*	lego-shell-adjust-line-width: save-excursion -> with-current-buffer to avoid	David Aspinall	2010-07-01
\| \| \| \|	spurious warning in Emacs 23.2
*	isar-shell-adjust-line-width: save-excursion -> with-current-buffer to avoid	David Aspinall	2010-07-01
\| \| \| \|	spurious warning in Emacs 23.2
*	proof-last-locked-span: save-excursion -> with-current-buffer to avoid	David Aspinall	2010-07-01
\| \| \| \|	spurious warning in Emacs 23.2
*	removed some old commands;	Makarius Wenzel	2010-06-29
\|
*	update from Isabelle2009-2;	Makarius Wenzel	2010-06-29
\|
*	Remove debug message	David Aspinall	2010-06-28
\|
*	Isabelle syntax update	David Aspinall	2010-06-28
\|