proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2011-04-26	Fix for Trac #397. Needs some exercise.	David Aspinall

2011-04-19	* small doc fix	Hendrik Tews

2011-04-15	* fix overwriting setq coq-prog-name before loading Proof General	Hendrik Tews
	* more complete callback listing in proof-action list doc
2011-04-13	proof-shell-insert-hook: Clean docstring, addressing #396.	David Aspinall

2011-04-13	Add proof-output-tooltips option to turn off output highlighting for people ↵	David Aspinall
	who read or edit by waving mouse at text
2011-03-14	- change to proof-restart-buffers for unlocking ancestors	Hendrik Tews
	- improve internal docs for unlocking
2011-03-09	Set version tag for new release.	David Aspinall

2011-02-23	Set version tag for new release.	David Aspinall

2011-02-14	put coq compilation feature into coq settings menu	Hendrik Tews

2011-01-31	Set version tag for new release.	David Aspinall

2011-01-31	Only make settings commands for dynamic settings which differ from their ↵	David Aspinall
	defaults
2011-01-31	Make proof-assistant-settings follow currently available dynamic settings, ↵	David Aspinall
	and keep possibly customized variables bound. Closes Trac #387.
2011-01-31	Support mouse action on modeline indicator for scripting mode	David Aspinall

2011-01-31	Improve handling of dynamic preferences. Addresses Trac #387.	David Aspinall

2011-01-31	Improve hint messages; use proof mode keymap.	David Aspinall

2011-01-31	Comments	David Aspinall

2011-01-31	Improve handling of trace buffer and tracing slow mode.	David Aspinall

2011-01-26	Add pg-autotest-start to allow debug startup, which doesn't catch errors.	David Aspinall

2011-01-26	- more info on the elements of proof-action-list; the COMMANDS	Hendrik Tews
	list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert.
2011-01-25	proof-deactivate-scripting: cleanup this function to make more	David Aspinall
	intelligible, also to properly support behaviour needed for `proof-no-fully-processed-buffer'.
2011-01-25	proof-fast-process-buffer: set to t also on Windows.	David Aspinall
	Untested, see http://proofgeneral.inf.ed.ac.uk/trac/ticket/308
2011-01-25	Bump/relax version numbers. Error for <23, warning for minor version mismatch.	David Aspinall

2011-01-25	Set version tag for new release.	David Aspinall

2011-01-25	proof-shell-kill-function: use our own busy loop, as proof-shell-wait	David Aspinall
	expects normal prover IO. Addresses http://proofgeneral.inf.ed.ac.uk/trac/ticket/384
2011-01-25	Dump Messages and PG Debug into log file, they have useful info.	David Aspinall

2011-01-24	- change 'span-delete-action in 'span-delete-actions, which is	Hendrik Tews
	now a list of functions to be run when the span is deleted. Use span-add-delete-action to add a delete action.
2011-01-24	Set version tag for new release.	David Aspinall

2011-01-23	Typo	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
	45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.
2011-01-23	proof-protected-process-or-retract: don't give failure error if nothing to do	David Aspinall
	Addresses Trac #383
2011-01-23	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-19	pg-create-in-span-context-menu: remove "Move up" and "Move down".	David Aspinall
	These don't seem to be very useful or reliable.
2011-01-19	pg-show-all-portions: protect against empty hash tables	David Aspinall

2011-01-19	Set version tag for new release.	David Aspinall

2011-01-18	- fixed stale load path problem with killing the proof shell in	Hendrik Tews
	the deactivation-hook
2011-01-18	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
	- fix quitting during compilation - substitute "compile" for "recompile" - added documentation
2011-01-18	Removing a debugging message.	Pierre Courtieu

2011-01-18	Set version tag for new release.	David Aspinall

2011-01-14	- move proof-no-fully-processed-buffer to generic/proof-config	Hendrik Tews
	- add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted
2011-01-14	- simple backward compatible change to invoke a function to	Hendrik Tews
	compute the command line arguments for a proof assistant
2011-01-12	Add preliminary support for multiple files for coq.	Hendrik Tews
	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
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