proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
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-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-23	proof-protected-process-or-retract: don't give failure error if nothing to do	David Aspinall
	Addresses Trac #383
2011-01-19	pg-show-all-portions: protect against empty hash tables	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-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
2010-10-11	proof-segment-up-to-using-cache: improve attempt	David Aspinall

2010-10-10	Fix debug message format	David Aspinall

2010-10-10	pg-span-name: improve docstring.	David Aspinall
	proof-complete-buffer-atomic: simplify. Add debug message for parser cache.
2010-10-10	Fix to last patch.	David Aspinall

2010-10-10	proof-assert-electric-terminator: prevent adding terminator if point is ↵	David Aspinall
	after it as well as before, as in PG 3.7. Fixes #371.
2010-10-01	Move utility span-make-modifying-removing-span to span.el	David Aspinall

2010-10-01	proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting ↵	David Aspinall
	input (no non-nil flags in queue)
2010-10-01	Adjust handling of insertion of newlines before next command.	David Aspinall

2010-09-29	Doc	David Aspinall

2010-09-08	mapcar -> mapc to fix compile error	David Aspinall

2010-09-08	Remove debug message	David Aspinall

2010-09-08	Improve/fix invisibility management, using buffer-invisibility-spec. Adjust ↵	David Aspinall
	span regions.
2010-09-08	Trivial comment change	David Aspinall

2010-09-08	Tidy comments.	David Aspinall

2010-09-07	proof-assert-electric-terminator: fix for proof-terminal-string, not char	David Aspinall

2010-08-27	Replace proof-terminal-char with proof-terminal-string.	David Aspinall

2010-08-27	Implement the eagerly anticipated Beyond Script Management Feature No.2 ↵	David Aspinall
	(i.e., automatic preview of next command)
2010-08-25	Fix compile: declare proof-interrupt-process	David Aspinall

2010-08-25	proof-retract-before-change: now interrupts are robust in Isabelle, try	David Aspinall
	interrupting if prover is busy before undoing. Refs Trac #293
2010-08-25	Bring syntactic context functions together	David Aspinall

2010-08-17	Autosend: don't autosend after undoing; add proof-shell-last-queuemode to ↵	David Aspinall
	support this.
2010-08-17	Whitespace	David Aspinall

2010-08-17	Clean up handling of pending interrupts, remove experimental ↵	David Aspinall
	proof-shell-interrupts-after-commit.
2010-08-16	Fix compile errors, update tags	David Aspinall

2010-08-15	Preliminary and experimental support for automatically sending commands.	David Aspinall

2010-08-13	proof-activate-scripting: make sure can succeed when	David Aspinall
	proof-activate-scripting-hook does nothing (case: switching buffers in Coq when there was an error)
2010-08-11	Support custom syntactic fontification. Split out pa macros.	David Aspinall

2010-08-08	proof-assert-electric-terminator: give more user-friendly error message if ↵	David Aspinall
	unparseable
2010-08-08	Checkdoc cleanups	David Aspinall

2010-08-03	proof-assert-electric-terminator: fix logic for inserting at buffer end	David Aspinall

2010-08-03	Move key binding for proof assistant keymap (fixes compilation bug)	David Aspinall

2010-08-03	save-some-buffers: only offer to save proof script buffers	David Aspinall

2010-08-03	Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.	David Aspinall

2010-07-08	Cleanups for save-excursion to avoid warnings in latest Emacs versions	David Aspinall

2009-12-03	Rework script span element hiding to avoid buffer-invisibility-spec. Add ↵	David Aspinall
	command elements.
2009-11-30	Fix for Trac #307.	David Aspinall

2009-11-30	Replace proof-locked-end -> proof-unprocessed-begin	David Aspinall

2009-11-28	Add `proof-script-sticky-error-face' and `proof-sticky-errors' setting.	David Aspinall

2009-10-15	proof-script-use-old-parser: remove configuration option and cleanup	David Aspinall

2009-10-14	Shorten comments	David Aspinall

2009-10-03	proof-script-generic-parse-cmdstart: set case-fold-search	David Aspinall
	proof-inside-string: added
2009-10-03	proof-assert-electric-terminator: repair so works at end of buffer	David Aspinall

2009-10-02	proof-retract-before-change: give error if prover busy	David Aspinall
	(see http://proofgeneral.inf.ed.ac.uk/trac/ticket/293)
2009-09-28	Functions find-and-forget and count-undos now return lists of commands	David Aspinall