proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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.
*	Includes commented code for Coq version of extent protocol	Healfdene Goguen	1997-11-13
\|
*	Changed pbp-change-goal so that it only "Show"s the goal pointed at.	Healfdene Goguen	1997-11-12
\|
*	Started modifications for emacs19 port.	Dilip Sequiera	1997-11-10
\|
*	Put in a workaround for a strange bug in comint which was finding a bunch	Dilip Sequiera	1997-11-10
\| \| \| \|	of ^G's from comint-get-old-input for some inexplicable reason.
*	Parameterize by proof-goal-hyp-fn in pbp-make-top-extent, to handle	Healfdene Goguen	1997-11-06
\| \| \| \| \| \| \|	Coq goals which start with text rather than simply ?n Updated 'let (ap 0)' in proof-shell-analyse structure, to be slightly more compatible with Coq pbp code
*	Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which is	Healfdene Goguen	1997-11-06
\| \| \| \|	simply old code for picking up goal or hypothesis for pbp
*	Assign new variable proof-goal-hyp-fn to coq-goal-hyp, which advances	Healfdene Goguen	1997-11-06
\| \| \| \|	over coq-goal-regexp to pick up goal for pbp
*	Updates to Coq fontlock tables	Healfdene Goguen	1997-11-06
\|
*	o implented proof-find-next-terminator available via C-c C-e	Thomas Kleymann	1997-10-31
\| \| \| \|	o fixed a bug in proof-done-retracting
*	Updates for coq, including:	Healfdene Goguen	1997-10-30
\| \| \| \| \| \|	* pbp-goal-command and pbp-hyp-command use proof-terminal-string * updates to keywords * fix for goal regexp
*	Updated comment about extent types	Healfdene Goguen	1997-10-24
\|
*	New indentation for lego-count-undos (smile)	Healfdene Goguen	1997-10-24
\|
*	Fixed coq-count-undos for comments	Healfdene Goguen	1997-10-24
\|
*	Changed order of "Inversion_clear" and "Inversion" so that former is	Healfdene Goguen	1997-10-24
\| \| \| \| \|	fontified first. Added "Print" to list of commands.
*	Updated proof-segment-up-to to take ""'s into account	Healfdene Goguen	1997-10-22
\| \| \| \| \| \|	Hence, << Cd "../x". >> works in Coq, and << echo "hello; world"; >> should work in LEGO But maybe we don't want "Cd"'s at all...
*	proof-active-terminator inside comment case fixed. Also maybe the	Dilip Sequiera	1997-10-17
\| \| \| \|	continuous pbp-buffer update bug.
*	Fixed coq-shell-prompt-pattern to reflect proof-id	Healfdene Goguen	1997-10-17
\| \| \| \| \|	Changed ";" to "." in coq-save-with-hole-regexp New modifications to syntax table to reflect actual use of symbols in Coq
*	Added "Induction" as tactic	Healfdene Goguen	1997-10-17
\|
*	fixed a bug in proof-process-active-terminator. Notice that it still	Thomas Kleymann	1997-10-17
\| \| \| \| \|	doesn't work when you are inside a comment and press the proof-terminal-char
*	Figured out display tables.	Dilip Sequiera	1997-10-16
\|
*	Merged Coq changes with main branch.	Dilip Sequiera	1997-10-16
\|
*	Merged Coq changes onto main branch	Dilip Sequiera	1997-10-16
\|
*	merged script management (1.10.2.18) with main branch	Thomas Kleymann	1997-10-16
\|
*	o merged script management (1.20.2.11) on the main branch	Thomas Kleymann	1997-10-16
\| \| \| \|	o fixed a bug in lego-find-and-forget due to new treatment of comments
*	proof-process-active-terminator is now an extension of	Thomas Kleymann	1997-10-14
\| \| \| \|	proof-assert-until-point (it was broken and looks healthier now)
*	* empty log message *	Thomas Kleymann	1997-10-13
\|
*	put script-management branch back on main branch	Thomas Kleymann	1997-10-13
\|
*	The package pbp is now integrated in the proof package	Thomas Kleymann	1997-10-13
\|
*	lego-count-undos is now aware that comments are treated separately	Thomas Kleymann	1997-10-13
\|
*	* empty log message *	Healfdene Goguen	1997-10-08
\|