proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	rewrote code from scratch: faster, easier to configure; now enabled by default;	Makarius Wenzel	2000-06-08
\|
*	settings for new indentation setup;	Makarius Wenzel	2000-06-08
\|
*	added proof-looking-at-safe, proof-looking-at-syntactic-context;	Makarius Wenzel	2000-06-08
\| \| \| \|	removed proof-indent-commands-regexp;
*	completely new indentation setup: faster, easier to configure;	Makarius Wenzel	2000-06-08
\| \| \| \|	now enabled by default;
*	basic setup for new indentation code;	Makarius Wenzel	2000-06-08
\|
*	proper indentation;	Makarius Wenzel	2000-06-08
\|
*	Improved indentation code; enabled by default;	Makarius Wenzel	2000-06-08
\|
*	Failed attempted hack to support ML files in isar mode (see comments in ↵	David Aspinall	2000-06-07
\| \| \| \|	isar-preprocessing).
*	Removed disable of simp tracing from enable/disable pr, desired ↵	David Aspinall	2000-06-07
\| \| \| \|	functionality now in Isabelle's update_thy for PG
*	Set version tag for new release.	David Aspinall	2000-06-06
\|
*	todo for C-c C-l to fix point	David Aspinall	2000-06-06
\|
*	Make distclean rather than clean do the CVS pruning.	David Aspinall	2000-06-06
\|
*	Added special hack for Isar to include proof-terminal-char in sent string.	David Aspinall	2000-06-06
\|
*	Allowed ; to terminate a command by including it in regexp for cmdstart	David Aspinall	2000-06-06
\| \| \| \|	Added completion for Isar keywords and X-symbol token names.
*	isar-save-with-hole-regexp: proof-no-regexp;	Makarius Wenzel	2000-06-05
\|
*	proof-indent-commands-regexp: use proof-no-regexp;	Makarius Wenzel	2000-06-05
\| \| \| \| \|	isar-global-save-command-p: more robust wrt. empty prev span (malformed!?); isar-preprocessing: fixed terminator regexp;
*	improved isabelle-verbatim-regexp: use \` \' instead of ^ $;	Makarius Wenzel	2000-06-05
\|
*	fixed proof-anchor-regexp: use \` instead of ^;	Makarius Wenzel	2000-06-05
\| \| \| \|	added proof-no-regexp;
*	Removed defunct comments	David Aspinall	2000-06-05
\|
*	Temporary bug fix to solve nil span error message	David Aspinall	2000-06-05
\|
*	Updated.	David Aspinall	2000-06-05
\|
*	proof-next-error, proof-display-some-buffers	David Aspinall	2000-06-05
\|
*	Added paragraph and index entry explaining prefix arguments,	David Aspinall	2000-06-05
\| \| \| \| \|	and some more on keystrokes, for the Emacs-impoverished users. Added doc of proof-display-some-buffers
*	Added proof-next-error to menu.	David Aspinall	2000-06-05
\|
*	Added settings for proof-next-error.	David Aspinall	2000-06-05
\| \| \| \| \|	Added switch off of simplifier tracing to quiet command (not good enough -- need help from Isabelle for that really).
*	Added miscellaneous commands section, with proof-display-some-buffers	David Aspinall	2000-06-05
\| \| \| \| \| \| \|	function. Bind C-c C-l to proof-display-some-buffers, add to buffer menu. Move start/exit to proof assistant specific menu. Added proof-next-error to menu.
*	proof-clean-buffer: clear next error flag if buffer is response.	David Aspinall	2000-06-05
\|
*	Tweaked some docstrings.	David Aspinall	2000-06-05
\| \| \| \| \|	Added proof-shell-next-error-regexp and friends. Bind proof-shell-next-error in proof-universal-keys.
*	Added proof-next-error.	David Aspinall	2000-06-05
\| \| \| \| \|	proof-shell-invisible-command: add terminator if it seems to be missing (after all: it's useful for users with C-c C-v).
*	Updated to add proof-next-error.	David Aspinall	2000-06-05
\|
*	fixed output syntax table;	Makarius Wenzel	2000-06-05
\|
*	proof-segment-up-to-cmdstart/end: use proof-re-search, proof-looking-at!	Makarius Wenzel	2000-06-04
\|
*	proof-re-search-forward/backward: observe proof-case-fold-search;	Makarius Wenzel	2000-06-04
\|
*	replaced isa-verbatim by isabelle-verbatim;	Makarius Wenzel	2000-06-04
\|
*	added isabelle-verbatim;	Makarius Wenzel	2000-06-04
\| \| \| \|	fixed proof-shell-pre-interrupt-hook: use isabelle-verbatim;
*	replaced isar-verbatim by isabelle-verbatim;	Makarius Wenzel	2000-06-04
\| \| \| \|	added isar-strip-terminators;
*	updated;	Makarius Wenzel	2000-06-04
\|
*	replaced isar-verbatim by isabelle-verbatim;	Makarius Wenzel	2000-06-04
\| \| \| \|	fixed output syntax table;
*	proof-segment-up-to-cmdstart: exclude leading blanks from command string;	Makarius Wenzel	2000-06-04
\|
*	improved proof-segment-up-to-cmdstart: handle overlap of command	Makarius Wenzel	2000-06-03
\| \| \| \|	prefix and comment/string (e.g. { vs {* in Isar);
*	{ } are back;	Makarius Wenzel	2000-06-03
\|
*	Added 3 entries in the Coq menu: Print Check and Hints	Pierre Courtieu	2000-06-02
\|
*	Set version tag for new release.	David Aspinall	2000-06-01
\|
*	Updated	David Aspinall	2000-06-01
\|
*	Added autoload	David Aspinall	2000-06-01
\|
*	Added links to latest manual	David Aspinall	2000-06-01
\|
*	File used to test new parsing mechanism.	David Aspinall	2000-06-01
\|
*	New test files for PG kit.	David Aspinall	2000-06-01
\|
*	Added proof-comment-{start,end}-regexp.	David Aspinall	2000-06-01
\| \| \| \| \| \|	Added proof-segment-up-to-{cmdstart,cmdend} and details of which is selected. Updated magic.
*	Updated	David Aspinall	2000-06-01
\|