proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Set version tag for new release.	David Aspinall	2012-01-10
\|
*	Tweak message and display model, in particular, make sure that when a	David Aspinall	2012-01-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	response appears above a goals output, the goals output is displayed second, so it is the one that remains visible to the user in the default 2-pane mode. This works with output like this in HOL Light: Warning: Free variables in goal: A, B val it : goalstack = 1 subgoal (1 total) ... and similar cases in Isabelle and Coq. The fix involves some ugly messing with the flags for clearing the response buffer (see `pg-response-maybe-erase'). This could surely be streamlined.
*	Improve configuration for HOL Light. Allow goals display to be prefixed by ↵	David Aspinall	2012-01-09
\| \| \| \|	ignored junk (val it : goalstack =).
*	proof-shell-end-goals-regexp doc: fix inaccuracy, goals always start	David Aspinall	2012-01-09
\| \| \| \|	at start of proof-shell-start-goals-regexp.
*	Temporarily enable HOL Light globally for testing	David Aspinall	2012-01-05
\|
*	* fix case where some existential is instantiated with the last proof command	Hendrik Tews	2012-01-04
\| \| \| \| \| \|	* protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message
*	Set version tag for new release.	David Aspinall	2012-01-04
\|
*	merge ProofTreeBranch into main trunk:	Hendrik Tews	2012-01-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof
*	Set version tag for new release.	David Aspinall	2011-12-07
\|
*	- protect proof-shell-handle-delayed-output against the case where	Hendrik Tews	2011-12-07
\| \| \| \| \|	proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals
*	fix a log of broken customization types	Hendrik Tews	2011-12-06
\|
*	use the start of proof-shell-end-goals-regexp, as documented	Hendrik Tews	2011-12-06
\|
*	Quick stab at support for switching to proof shell when interactive support ↵	David Aspinall	2011-11-15
\| \| \| \|	expected, see Trac #430
*	Add fix and regression test for Trac #138	David Aspinall	2011-10-17
\|
*	Set version tag for new release.	David Aspinall	2011-10-17
\|
*	Attempt to support stricter bytecomp flags	David Aspinall	2011-10-17
\|
*	Remove dependency of pg-movie on pg-user	David Aspinall	2011-10-17
\|
*	Set version tag for new release.	David Aspinall	2011-10-13
\|
*	Patch from Tom Prince to fix Emacs 24 byte compilation (replace ↵	David Aspinall	2011-10-13
\| \| \| \|	interactive-p with called-interactively-p)
*	To fix pgshell mode, restore proof-shell-insert support for a single string ↵	David Aspinall	2011-10-13
\| \| \| \|	argument and allow nil setting for proof-shell-start-goals-regexp.
*	Set version tag for new release.	David Aspinall	2011-10-03
\|
*	fix #426	Hendrik Tews	2011-09-27
\|
*	Set version tag for new release.	David Aspinall	2011-09-19
\|
*	proof-full-annotation: default to nil	David Aspinall	2011-09-18
\|
*	Set version tag for new release.	David Aspinall	2011-09-16
\|
*	fix #421 with solution 1	Hendrik Tews	2011-09-14
\|
*	proof-electric-terminator: allow a prefix argument to avoid electric action.	David Aspinall	2011-09-14
\| \| \| \|	Addresses Trac #422
*	# User Robin Green <greenrd@greenrd.org>	David Aspinall	2011-09-14
\| \| \| \|	Use correct customisation widget for variable-length list of strings
*	Fix typo	David Aspinall	2011-09-14
\|
*	Remove contentious call to set-process-query-on-exit-flag, ref Trac#424	David Aspinall	2011-09-14
\|
*	Fix proof-shell-exit optional argument with (interactive) thanks to	Pierre Courtieu	2011-09-11
\| \| \| \|	Erik Martin-Dorel.
*	Capitalize menu items	David Aspinall	2011-08-24
\|
*	Set version tag for new release.	David Aspinall	2011-08-24
\|
*	Remove PG prefix from toolbar button names (needed for disambiguity in older ↵	David Aspinall	2011-08-23
\| \| \| \|	Emacsen, displayed in Emacs 24 UI)
*	Set version tag for new release.	David Aspinall	2011-08-23
\|
*	Set version tag for new release.	David Aspinall	2011-06-22
\|
*	Set version tag for new release.	David Aspinall	2011-06-22
\|
*	Set version tag for new release.	David Aspinall	2011-06-10
\|
*	Set version tag for new release.	David Aspinall	2011-06-10
\|
*	Set version tag for new release.	David Aspinall	2011-06-09
\|
*	Add autoload.	David Aspinall	2011-06-09
\|
*	- fix for #408: Only use the buffer name in	Hendrik Tews	2011-06-08
\| \| \| \| \|	coq-compile-response-buffer - fix typo elsewhere
*	Set version tag for new release.	David Aspinall	2011-06-07
\|
*	proof-undo-and-delete-last-successful-command: obey spec (Trac #407)	David Aspinall	2011-06-03
\|
*	Set version tag for new release.	David Aspinall	2011-06-01
\|
*	Set version tag for new release.	David Aspinall	2011-05-30
\|
*	Trac#403: wait for retraction to complete before returning, to	David Aspinall	2011-05-30
\| \| \| \|	avoid hitting read only error in calling command.
*	ensure (integerp proof-segment-up-to-cache-end), fixes Trac #404	David Aspinall	2011-05-27
\|
*	Set version tag for new release.	David Aspinall	2011-05-27
\|
*	proof-retract-before-change: fix Trac #403 (at least partially) by	David Aspinall	2011-05-26
\| \| \| \| \|	removing restriction during automatic retraction so proof-retract-until-point behaves correctly.