proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Coqtop always restarted when switching script buffer.	Pierre Courtieu	2015-03-03
\| \| \| \| \| \|	This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options.
*	Fixed read-only error for compile before require option.	Pierre Courtieu	2015-02-11
\| \| \| \| \| \|	the emacs bug seems solved: the error with read-only always occur whatever locale is used. So I toggle read-only off in coq-compile-response.
*	Fix coq project parsing and interpreting for coq v8.5.	Pierre Courtieu	2015-01-27
\|
*	fixed indentation (lexing of 'with') + made local coq-load-path.	Pierre Courtieu	2014-12-30
\|
*	- fix asserting when parallel background compilation is in progress	Hendrik Tews	2013-01-03
\| \| \| \|	- fix aborting background compilation on error
*	all-cpus option for coq-max-background-compilation-jobs	Hendrik Tews	2012-11-14
\|
*	update documentation	Hendrik Tews	2012-11-14
\|
*	- first version of parallel asynchronous compilation for coq in	Hendrik Tews	2012-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used
*	move ancestor locking back into specific part	Hendrik Tews	2012-11-06
\|
*	move ancestor locking/unlocking to coq-compile-common	Hendrik Tews	2012-11-05
\|
*	move buffer saving to coq-compile-common	Hendrik Tews	2012-11-05
\|
*	make coq-include-options independent of current buffer	Hendrik Tews	2012-11-03
\|
*	move another 2 functions into coq-compile-common	Hendrik Tews	2012-11-03
\|
*	move function for coq-compile-response-buffer to coq-compile-common.el	Hendrik Tews	2012-11-01
\|
*	move some more material into coq-compile-common	Hendrik Tews	2012-10-30
\|
*	move general part of compilation into coq-compile-common.el	Hendrik Tews	2012-10-30