proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	* empty log message *	Patrick Loiseleur	1999-06-08
\|
*	removed superficial space;	Makarius Wenzel	1999-05-25
\|
*	I've added the custom option 'prog-name-guess' in the generic part and	Patrick Loiseleur	1999-05-17
\| \| \| \| \| \| \| \| \|	the function coq-guess-command-line in the coq part. Every prover should have the functon *-guess-command-line that uses, for example, the output of "make -n" to guess the correct command line options of the prover. Patrick
*	Experimental bug fix for Solaris problem	David Aspinall	1999-01-15
\|
*	Beginnings of x-symbol support.	David Aspinall	1998-12-18
\|
*	Fixes for FSF Emacs handling of processes, kill buffer hooks,	David Aspinall	1998-12-15
\| \| \| \|	and live/dead overlays.
*	made many minor changes to the documentation	Thomas Kleymann	1998-12-15
\|
*	Disabled hack for proof-shell-process-file which allowed	David Aspinall	1998-12-11
\| \| \| \| \| \| \| \| \| \| \|	empty string to stand for filename of current scripting buffer. This added the current script buffer onto the included files list immediately processing it began (if it began with something creating a mark). However, I removed the check for the current scripting buffer so that that could correctly be marked atomic for Isabelle at other times. This resulted in current buffer being marked atomic, and errors. Are there still more errors?
*	Removed proof-send, now use proof-shell-insert instead.	David Aspinall	1998-12-11
\| \| \| \| \|	Removed proof-preprocess-input hook function, Paul Callaghan can now use proof-shell-insert-hook instead for his need.
*	Disabled span-making part of proof-shell-analyse structure for Emacs 20.3	David Aspinall	1998-12-11
\|
*	Made point stay at top of goals buffer and bottom of response buffer	David Aspinall	1998-12-10
\|
*	o special characters are no longer displayed in (16Bit) FSF GNU Emacs	Thomas Kleymann	1998-12-08
\| \| \| \| \| \| \|	20.3 o however, there is still a mysterious bug in 'proof-shell-analyse-structure' when processing lego/example.l
*	Added proof-shell-preprocess-command for Paul Callaghan.	David Aspinall	1998-12-07
\|
*	BUG fix: proof-shell-message with str's containing format characters.	David Aspinall	1998-11-26
\| \| \| \| \| \|	BUG fix: kill-function: another chance to catch process sentinel added. BUG fix: FSF Emacs minor-mode-alist BUG fix: FSF Emacs problem with proof-shell-insert mess. Still probs.
*	Got rid of an error message in case of process early exiting.	David Aspinall	1998-11-25
\|
*	Docstring improvements.	David Aspinall	1998-11-25
\|
*	FSF Emacs fix for buffer-file-truename, which is the	David Aspinall	1998-11-25
\| \| \| \|	abbreviated form of file-truename!
*	Improved kill function. Added process sentinel to watch for process exiting.	David Aspinall	1998-11-25
\|
*	Replaced proof-pbp-buffer with proof-goals-buffer.	David Aspinall	1998-11-25
\|
*	In filter: minor improvement for when proof-shell-wakeup-char is set.	David Aspinall	1998-11-25
\| \| \| \| \| \| \|	In proof-shell-handle-error: Make action list empty to prevent proof shell filter seeing same error over and over in case user types directly in shell buffer after an error.
*	Use make-local-hook instead of make-local-variable	David Aspinall	1998-11-25
\|
*	Fixed up exit hook (still buggy)	David Aspinall	1998-11-25
\|
*	Docstring fixes, minor improvements.	David Aspinall	1998-11-25
\|
*	Improved docstrings	David Aspinall	1998-11-25
\|
*	Docstring fixes	David Aspinall	1998-11-25
\|
*	Reimplemented functions to shut down and restart proof process.	David Aspinall	1998-11-20
\| \| \| \| \| \|	Scrapped proof-shell-exit-hook. Added proof-shell-quit-cmdd, proof-shell-restart-comd Fancier Scripting indicator for active scripting buffer.
*	BIG CHANGES -- SORRY!	David Aspinall	1998-11-20
\| \| \| \| \| \| \| \|	Replaced proof-script-buffer-list with proof-script-buffer. The list was causing too much confusion and nasty bugs used with Isabelle multiple files. Implemented proof-script-buffers and proof-restart-all-buffers, other functions.
*	. Changed behaviour of retracting current scripting buffer:	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \| \| \|	now it nukes proof-script-buffer-list (possibly unecessarily). Before, current scripting buffer was silently preserved in case it was retracted, but this means that proof-activate-scripting-hook was not run when scripting was begun again in the buffer, which left PG in an inconsistent state with respect to included files (in Isabelle). URGENT: must check this is okay with LEGO.
*	. bug fix for proof-shell-live-buffer.	David Aspinall	1998-11-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	. bug fix for proof-shell-filter for case that prompt isn't seen in first output chunk. . bug fix of handling urgent messages in delayed output: skip past the last one seen. Previously messages were put into the response buffer twice (first time highlighted). Don't clear the response buffer between urgent messages and delayed output within the same prompt-delimited region. . big improvement of display handling for response buffer, via new function proof-shell-maybe-erase-response. . added proof-shell-clear-response-regexp . docstring fixes.
*	Rashly fixed a suspicious looking nested use of set-buffer. Docstrings.	David Aspinall	1998-11-12
\|
*	Renamed proof-mode-name -> proof-general-name.	David Aspinall	1998-11-12
\| \| \| \| \| \|	Reimplemented configuration for fume-menu. Now works for named goals, named saves, and (e.g. lego) both! Removed some FIXME's.
*	Added buffers menu, and added shared menu to shell and response buffers.	David Aspinall	1998-11-10
\|
*	Fixed bug for when proof-rsh-command is empty	David Aspinall	1998-11-10
\|
*	Refresh response buffer when goals buffer is refreshed.	Thomas Kleymann	1998-11-10
\|
*	Added proof-rsh-command to help complete documentation (was allocated	David Aspinall	1998-11-09
\| \| \| \|	to tms but he said he wouldn't get around to it)
*	Being pedantic about variables versus predicates, renamed prog-name-ask-p.	David Aspinall	1998-11-03
\|
*	Removed FIXME	David Aspinall	1998-11-03
\|
*	A* Fix display handling problems (tms, all week)	Thomas Kleymann	1998-11-03
\| \| \| \|	Done. :-)
*	Quick fix for multiple file problem when current scripting buffer is ↵	David Aspinall	1998-11-02
\| \| \| \|	retracted by prover.
*	Proof General no longer changes selected window/buffer under your feet.	Thomas Kleymann	1998-11-02
\|
*	fixed minor bugs	Thomas Kleymann	1998-11-02
\|
*	o added support for byte-compilation	Thomas Kleymann	1998-11-01
\| \| \| \| \| \| \|	o removed hhg tags in todo o fixed font-lock for FSF Emacs 20.2 o ensured that goals buffer is updated for longer queues o fixed a bug in proof-universal-keys-only-mode
*	implemented new buffer model. The goals buffer is now exclusively	Thomas Kleymann	1998-10-30
\| \| \| \|	reserved for goals.
*	replaced some occurences of (current-buffer) by proof-shell-buffer to	Thomas Kleymann	1998-10-30
\| \| \| \|	make code more robust
*	Fixed bug in proof-shell-process-urgent-message (preserve point).	David Aspinall	1998-10-29
\|
*	rearranged code to avoid compiler warning messages	Thomas Kleymann	1998-10-28
\|
*	Continuing mods for cleaner byte compile	David Aspinall	1998-10-27
\|
*	More fixes for cleaner byte compile.	David Aspinall	1998-10-27
\|
*	Removed eval-when-compile around define-derived-mode, it don't work.	David Aspinall	1998-10-27
\|
*	Fixed up proof-script.el for clean byte compile	David Aspinall	1998-10-27
\|