proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Simpler procedure for compiling emacs lisp.	Healfdene Goguen	1998-05-06
\| \| \| \|	Added coq-info-dir so that script-management.info can be hard-coded.
*	Coq now restarts if going back to beginning of proof.	Healfdene Goguen	1998-05-05
\|
*	Updated to include changes for emacs19.	Healfdene Goguen	1998-05-05
\| \| \| \| \| \| \|	Also includes some changes for "Definition" problem in Coq, where Definition couldn't be used for proof scripts. Finally, modified proof-dependencies-xemacs code to fix problem that undoing to (point-min) meant you couldn't type at first character.
*	Simple white-space changes.	Healfdene Goguen	1998-05-05
\|
*	Removed because its functionality is subsumed by the xemacs and	Healfdene Goguen	1998-05-05
\| \| \| \|	emacs19 files.
*	Dependencies of proof mode for xemacs	Healfdene Goguen	1998-05-05
\| \| \| \| \|	There may be one or two areas that can be unified with emacs19 dependencies.
*	Dependencies of proof mode for emacs19	Healfdene Goguen	1998-05-05
\| \| \| \|	Still in progress!
*	Added lego-goal-command-p to fix Coq's problem with "Definition".	Healfdene Goguen	1998-05-05
\| \| \| \|	Removed lego-killref from menu.
*	Made updates to fix problem with Definition, which couldn't be	Healfdene Goguen	1998-05-05
\| \| \| \| \| \| \| \|	used with proof scripts. Removed some useless declarations. Removed Abort from menu. Now Reset's if user undoes to beginning of proof. Added command to increase undo limit for Coq, and set default to 100.
*	Added CoInductive.	Healfdene Goguen	1998-05-05
\| \| \| \| \|	Made updates to reflect problem with "Definition", which couldn't be used with proof scripts.
*	Basic instructions that come with package	Healfdene Goguen	1998-05-05
\|
*	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1998-05-01
\|\ \| \| \| \|	branch.
\| *	X-Symbol version 4.45 beta	David Aspinall	1998-05-01
\| \|
* \|	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1998-05-01
\|\\| \| \| \| \|	branch.
\| *	Version 4.5 (beta?) sent by CW, as a package distrib.	David Aspinall	1998-05-01
\| \|
* \|	removed explicit reference to a binary in ctm's home directory	Thomas Kleymann	1998-04-27
\| \|
* \|	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1998-04-17
\|\\| \| \| \| \|	branch.
\| *	X-Symbol version 4.45 beta	David Aspinall	1998-04-17
\| \|
* \|	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1998-04-17
\|\\| \| \| \| \|	branch.
\| *	Version 4.5 (beta?) sent by CW, as a package distrib.	David Aspinall	1998-04-17
\| \|
* \|	added support for etags at generic proof level	Thomas Kleymann	1998-03-25
\| \|
* \|	* empty log message *	Thomas Kleymann	1998-03-24
\| \|
* \|	prioritised	Thomas Kleymann	1998-02-11
\| \|
* \|	* empty log message *	Thomas Kleymann	1998-02-10
\| \|
* \|	added Dnf to lego-undoable-commands-regexp	Thomas Kleymann	1998-02-10
\| \|
* \|	This commit was generated by cvs2git to track changes on a CVS vendor	David Aspinall	1998-01-26
\|\\| \| \| \| \|	branch.
\| *	X-Symbol version 4.45 beta	David Aspinall	1998-01-26
\| \|
* \|	Commented the code of proof.el and lego.el a bit. Made a minor change	Dilip Sequiera	1998-01-16
\| \| \| \| \| \| \| \| \| \|	to the way errors are handled, so that any delayed output is inserted in the buffer before the error message is printed.
* \|	Added coq-shell-cd	Healfdene Goguen	1998-01-15
\| \| \| \| \| \| \| \|	Some new fontlocks
* \|	Updated method of defining proof-shell-cd to be consistent with other	Healfdene Goguen	1998-01-15
\| \| \| \| \| \| \| \| \| \|	proof-assistant-dependent variables. Added ctrl-button1 to copy selected region to end of locked region
* \|	One needed change for coq included	Healfdene Goguen	1998-01-15
\| \|
* \|	o added support for remote proof processes	Thomas Kleymann	1998-01-12
\| \| \| \| \| \| \| \|	o bound C-c C-z to 'proof-frob-locked-end
* \|	improved fume support	Thomas Kleymann	1998-01-05
\| \|
* \|	fixed a bug in the indenting functions	Thomas Kleymann	1998-01-05
\| \|
* \|	* empty log message *	Thomas Kleymann	1997-12-18
\| \|
* \|	o introduced proof-shell-handle-error-hook and bount it by default to	Thomas Kleymann	1997-12-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	proof-goto-end-of-locked-if-pos-not-visible-in-window (also new) o proof-find-next-terminator now also works inside a locked region o implemented proof-process-buffer which is by default bount to C-c C-b
* \|	Noted bug in popup-eager-annotation	Dilip Sequiera	1997-11-26
\| \|
* \|	Added C-c C-s to run "Search" in Coq.	Healfdene Goguen	1997-11-26
\| \| \| \| \| \| \| \| \| \|	Moved coq-goal-with-hole-regexp etc to coq-fontlock. Removed various superfluous definitions for COQPATH etc.
* \|	A few new suggestions	Healfdene Goguen	1997-11-26
\| \|
* \|	Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1	Healfdene Goguen	1997-11-26
\| \|
* \|	o The response buffer focusses on the first goal	Thomas Kleymann	1997-11-26
\| \| \| \| \| \| \| \| \| \| \| \|	o If proof-retract-until-point is is invoked outside a locked region, the last successfully processed command is undone. o Added support for func-menu
* \|	o simplified code:	Thomas Kleymann	1997-11-26
\| \| \| \| \| \| \| \| \| \| \| \|	lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now used for lego-font-lock-keywords-1 as well o improved lego-find-and-forget
* \|	simplified code:	Thomas Kleymann	1997-11-26
\| \| \| \| \| \| \| \| \| \|	lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now used for lego-font-lock-keywords-1 as well
* \|	Added proof-execute-minibuffer-cmd and scripting minor mode.	Dilip Sequiera	1997-11-24
\| \|
* \|	Added proof-global-p to test whether a 'vanilla should be lifted above	Healfdene Goguen	1997-11-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	active lemmas. Separated proof-lift-global as separate command to lift global declarations above active lemmas. Fixed usual problem that 'cmd is nil for comments in this code. Made lifting globals start from beginning of file rather than go backwards. Fixed bug in pbp code proof-shell-analyse-structure, where stack wasn't cleared for new goal-hyp's.
* \|	Fixed outstanding things to be updated in Coq.	Healfdene Goguen	1997-11-20
\| \|
* \|	Added lego-global-p as always false, but for consistency with Coq mode.	Healfdene Goguen	1997-11-20
\| \| \| \| \| \| \| \|	Changed [meta (control i)] to [meta tab] in key definition.
* \|	Added coq-global-p for global declarations and definitions. These now	Healfdene Goguen	1997-11-20
\| \| \| \| \| \| \| \| \| \| \| \|	get lifted in the same way as lemmas. Changed [meta (control i)] to [meta tab] in key definition. Changed menu, and made help in menu refer to info mode.
* \|	Added indentation for lego-mode.	Dilip Sequiera	1997-11-18
\| \|
* \|	Added some magic commands: proof-frob-locked-end, proof-try-command,	Dilip Sequiera	1997-11-17
\| \| \| \| \| \| \| \| \| \|	proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET.