proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Remove dead code	David Aspinall	2011-01-25
\|
*	Remove proof-shell-wait that causes deadlock with new multiple-file code.	David Aspinall	2011-01-25
\|
*	proof-shell-kill-function: use our own busy loop, as proof-shell-wait	David Aspinall	2011-01-25
\| \| \| \| \|	expects normal prover IO. Addresses http://proofgeneral.inf.ed.ac.uk/trac/ticket/384
*	Dump Messages and PG Debug into log file, they have useful info.	David Aspinall	2011-01-25
\|
*	- change 'span-delete-action in 'span-delete-actions, which is	Hendrik Tews	2011-01-24
\| \| \| \| \|	now a list of functions to be run when the span is deleted. Use span-add-delete-action to add a delete action.
*	Set version tag for new release.	David Aspinall	2011-01-24
\|
*	Add News for 4.1	David Aspinall	2011-01-24
\|
*	updated theory headers;	Makarius Wenzel	2011-01-23
\|
*	Typo	David Aspinall	2011-01-23
\|
*	Documentation updates	David Aspinall	2011-01-23
\|
*	proof-shell-exit: mention quit command and quit timeout in doc	David Aspinall	2011-01-23
\|
*	Make proof-shell-quit-timeout a prover-specific customize option, default to ↵	David Aspinall	2011-01-23
\| \| \| \|	45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.
*	proof-protected-process-or-retract: don't give failure error if nothing to do	David Aspinall	2011-01-23
\| \| \| \|	Addresses Trac #383
*	Save the log file without querying user on exit	David Aspinall	2011-01-23
\|
*	Kill prover process without asking on Emacs exit	David Aspinall	2011-01-23
\|
*	Fix typo	David Aspinall	2011-01-23
\|
*	- use time-less-p	Hendrik Tews	2011-01-21
\| \| \| \| \| \| \|	- delete previous-head, simplify loop - coq 8.2 compatibility - describe bug for killing completely asserted active buffers in coq/ex/test-cases/retract-completely-asserted
*	pg-create-in-span-context-menu: remove "Move up" and "Move down".	David Aspinall	2011-01-19
\| \| \| \|	These don't seem to be very useful or reliable.
*	pg-show-all-portions: protect against empty hash tables	David Aspinall	2011-01-19
\|
*	Set version tag for new release.	David Aspinall	2011-01-19
\|
*	Update date stamps	David Aspinall	2011-01-19
\|
*	- switch off automatic compilation for coq to not surprise users	Hendrik Tews	2011-01-19
\| \| \| \|	too much
*	- improved doc nodes Using file variables and Locking Ancestors	Hendrik Tews	2011-01-19
\|
*	- fixed stale load path problem with killing the proof shell in	Hendrik Tews	2011-01-18
\| \| \| \|	the deactivation-hook
*	- implemented coq-lock-ancestors as described in the docs already	Hendrik Tews	2011-01-18
\|
*	Add multiple file test case	David Aspinall	2011-01-18
\|
*	Alternative fix to #382.	David Aspinall	2011-01-18
\|
*	set proof-auto-action-when-deactivating-scripting to 'retract,	David Aspinall	2011-01-18
\| \| \| \|	to stop new multiple file handling for Coq interactive queries
*	Localise compilation fix for dynamic scope of `queueitems\'.	David Aspinall	2011-01-18
\|
*	- fixed compilation errors	Hendrik Tews	2011-01-18
\|
*	- fix broken external compilation	Hendrik Tews	2011-01-18
\| \| \| \| \| \|	- fix quitting during compilation - substitute "compile" for "recompile" - added documentation
*	Removing a debugging message.	Pierre Courtieu	2011-01-18
\|
*	Set version tag for new release.	David Aspinall	2011-01-18
\|
*	Fix trac 382 by not setting save-abbrevs.	Pierre Courtieu	2011-01-18
\|
*	fix problems in test cases	Hendrik Tews	2011-01-17
\| \| \| \|	coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir
*	set a non-temporary email address	Hendrik Tews	2011-01-14
\|
*	- more coq test cases (some with surprising and embarrassing bugs)	Hendrik Tews	2011-01-14
\|
*	Update dates and versions	David Aspinall	2011-01-14
\|
*	Add new CVS users to DEVELOPERS list.	David Aspinall	2011-01-14
\|
*	- move proof-no-fully-processed-buffer to generic/proof-config	Hendrik Tews	2011-01-14
\| \| \| \| \| \|	- add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted
*	- simple backward compatible change to invoke a function to	Hendrik Tews	2011-01-14
\| \| \| \|	compute the command line arguments for a proof assistant
*	- Remove nonfunctional Add LoadPath code.	Hendrik Tews	2011-01-14
\| \| \| \| \| \| \| \| \|	- Use coqdep now to map the required module to a file name. "Require Arith." works now, but coqdep fails on "Require Arith.Le.". - Remove the coq-internal-load-path hash and all related function. Coq's load path logic is too complicated to reimplement that in ProofGeneral
*	Add preliminary support for multiple files for coq.	Hendrik Tews	2011-01-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names
*	Tweak text wrt http://proofgeneral.inf.ed.ac.uk/trac/ticket/355	David Aspinall	2011-01-12
\|
*	Set version tag for new release.	David Aspinall	2011-01-12
\|
*	Remove comment	David Aspinall	2011-01-12
\|
*	Type-check on integer settings	David Aspinall	2011-01-12
\|
*	Fix quoting in 'float patch.	David Aspinall	2011-01-12
\|
*	Add additional support for pgipfloat type	David Aspinall	2011-01-11
\|
*	'float -> 'number	David Aspinall	2011-01-11
\|