proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.	Erik Martin-Dorel	2017-08-15
\| \| \| \|	This commit address ProofGeneral/PG#193.
*	Remove default key-binding for proof-electric-terminator-toggle.	Erik Martin-Dorel	2017-03-03
\| \| \| \|	Close ProofGeneral/PG#160
*	proof-retract-before-change: Fix #41 by saving/restoring the match data.	Erik Martin-Dorel	2016-09-25
\|
*	Reset proof-script-buffer to nil if -ready-prover fails	Clément Pit--Claudel	2016-06-10
\| \| \| \|	Fixes #65
*	Fixing #25.	Pierre Courtieu	2016-01-06
\| \| \| \|	proof-script-buffer was not set before calling proof-shell-ready-prover.
*	proof-retract-command-hook added + more auto adjust width in coq mode.	Pierre Courtieu	2015-10-13
\|
*	proof-assert-command-hook added + Auto adjust width in coq mode.	Pierre Courtieu	2015-10-12
\| \| \| \| \| \| \|	This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing).
*	Don't mess with overlay priorities.	Stefan Monnier	2014-06-06
\|
*	Add option proof-layout-windows-on-visit-file, addressing Trac #444	David Aspinall	2012-08-16
\|
*	fix 443 by enforcing that the prover is not busy in proof-retract-until-point	Hendrik Tews	2012-08-14
\|
*	* generic/pg-user.el (which-func-modes): Fix compiler declaration.	Stefan Monnier	2012-06-29
\| \| \| \|	* generic/proof-site.el (assistants): Fix regexp.
*	Made a small change in generic code about the setting of	Pierre Courtieu	2012-06-09
\| \| \| \| \| \| \|	comment-start-skip: if it is already set then proof-script should not change it. Ultimately if David approves we should moreover fix the setting itself which is bugged. coq-mode now sets this variable by itself.
*	Patch from Tom Prince to fix Emacs 24 byte compilation (replace ↵	David Aspinall	2011-10-13
\| \| \| \|	interactive-p with called-interactively-p)
*	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
*	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
\|
*	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.
*	Patch for Trac#400.	David Aspinall	2011-05-16
\|
*	Tweak for `proof-segment-up-to-using-cache': better handling of	David Aspinall	2011-05-12
\| \| \| \|	proof-last-edited-low-watermark.
*	Attempted fix for `proof-segment-up-to-using-cache', re	David Aspinall	2011-05-12
\| \| \| \|	http://proofgeneral.inf.ed.ac.uk/trac/ticket/395
*	- flushed proof-done-advancing-require-function and	Hendrik Tews	2011-05-05
\| \| \| \| \|	proof-shell-require-command-regexp - TAGS updated to really flush them
*	Fix for Trac #397. Needs some exercise.	David Aspinall	2011-04-26
\|
*	Add proof-output-tooltips option to turn off output highlighting for people ↵	David Aspinall	2011-04-13
\| \| \| \|	who read or edit by waving mouse at text
*	- change to proof-restart-buffers for unlocking ancestors	Hendrik Tews	2011-03-14
\| \| \| \|	- improve internal docs for unlocking
*	Support mouse action on modeline indicator for scripting mode	David Aspinall	2011-01-31
\|
*	proof-deactivate-scripting: cleanup this function to make more	David Aspinall	2011-01-25
\| \| \| \| \|	intelligible, also to properly support behaviour needed for `proof-no-fully-processed-buffer'.
*	- 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.
*	proof-protected-process-or-retract: don't give failure error if nothing to do	David Aspinall	2011-01-23
\| \| \| \|	Addresses Trac #383
*	pg-show-all-portions: protect against empty hash tables	David Aspinall	2011-01-19
\|
*	- 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
*	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
*	proof-segment-up-to-using-cache: improve attempt	David Aspinall	2010-10-11
\|
*	Fix debug message format	David Aspinall	2010-10-10
\|
*	pg-span-name: improve docstring.	David Aspinall	2010-10-10
\| \| \| \| \|	proof-complete-buffer-atomic: simplify. Add debug message for parser cache.
*	Fix to last patch.	David Aspinall	2010-10-10
\|
*	proof-assert-electric-terminator: prevent adding terminator if point is ↵	David Aspinall	2010-10-10
\| \| \| \| \| \|	after it as well as before, as in PG 3.7. Fixes #371.
*	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	2010-10-01
\| \| \| \|	input (no non-nil flags in queue)
*	Adjust handling of insertion of newlines before next command.	David Aspinall	2010-10-01
\|
*	Doc	David Aspinall	2010-09-29
\|
*	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	2010-09-08
\| \| \| \|	span regions.
*	Trivial comment change	David Aspinall	2010-09-08
\|
*	Tidy comments.	David Aspinall	2010-09-08
\|
*	proof-assert-electric-terminator: fix for proof-terminal-string, not char	David Aspinall	2010-09-07
\|
*	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	2010-08-27
\| \| \| \|	(i.e., automatic preview of next command)