proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Fix remaining uses of CL; Make files more declarative	Stefan Monnier	2018-12-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f), so loading a file should "no effect". Fix the most obvious such effects: the splash screen and the autotests by moving those effects into a function. * coq/coq-autotest.el: Make it declarative. Use lexical-binding. (coq-autotest): New function holding the code that used to be at top-level. * generic/proof.el: Use lexical-binding. Don't call proof-splash-message just because we're being loaded. * generic/proof-script.el: Use lexical-scoping; fix all warnings. (pg-show-all-portions): Simplify the code with a closure. (proof-activate-scripting): Declare activated-interactively as dyn-scoped. (proof--splash-done): New var. (proof-mode): Call proof-splash-message upon first use. * generic/proof-splash.el (proof-splash-message): Don't check byte-compile-current-file now that we're only called when the mode is activated. * acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'. * coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²). * coq/coq-seq-compile.el: * coq/coq-par-test.el: * coq/coq-par-compile.el: Fix leftover uses of CL's `assert`. * generic/proof-utils.el: * generic/pg-movie.el: * etc/testsuite/pg-test.el: * coq/coq-syntax.el: Fix leftover uses of CL's `incf`. * generic/pg-autotest.el: Fix leftover uses of CL's `decf`. * obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use of CL's `loop`. * generic/pg-user.el (proof-add-completions): Do nothing if no proof-assistant is set yet (i.e. during byte-compilation). (byte-compile-current-file): No need to test this any more. * generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat. Remove unnecessary "\\(?:...\\)". (proof-regexp-alt): Redefine in terms of proof-regexp-alt-list.
*	Fix most doc issues raised by (checkdoc)	Erik Martin-Dorel	2018-08-23
\|
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	Fix incorrect assumption that noninteractive == byte-compiling	Clément Pit--Claudel	2017-03-08
\| \| \| \| \|	The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
*	small typo fixes	Hendrik Tews	2012-11-13
\|
*	Fixed a bug in three windows mode.	Pierre Courtieu	2012-09-25
\|
*	Three windows mode is back as the default mode.	Pierre Courtieu	2012-08-31
\|
*	Changed the behaviour of proof-layout-windows. Now it follows the	Pierre Courtieu	2012-08-31
\| \| \| \|	'horizontal 'vertical 'smart policy.
*	Setting nil by default the option to create resp and goals buffer	Pierre Courtieu	2012-08-31
\| \| \| \|	immediately when opening a file.
*	Add option proof-layout-windows-on-visit-file, addressing Trac #444	David Aspinall	2012-08-16
\|
*	Add user option proof-next-command-insert-space.	David Aspinall	2012-08-14
\|
*	fix #426	Hendrik Tews	2011-09-27
\|
*	proof-full-annotation: default to nil	David Aspinall	2011-09-18
\|
*	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
*	proof-fast-process-buffer: set to t also on Windows.	David Aspinall	2011-01-25
\| \| \| \|	Untested, see http://proofgeneral.inf.ed.ac.uk/trac/ticket/308
*	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
*	Use parser cache by default.	David Aspinall	2010-10-11
\|
*	proof-script-command-separator: remove; proof-one-command-per-line becomes ↵	David Aspinall	2010-10-01
\| \| \| \|	prover specific.
*	Implement the eagerly anticipated Beyond Script Management Feature No.2 ↵	David Aspinall	2010-08-27
\| \| \| \|	(i.e., automatic preview of next command)
*	proof-fast-process-buffer: switch on by default if looks like Mac port (ns ↵	David Aspinall	2010-08-22
\| \| \| \|	feature)
*	Add Fast Process Buffer option	David Aspinall	2010-08-19
\|
*	Preliminary and experimental support for automatically sending commands.	David Aspinall	2010-08-15
\|
*	Checkdoc cleanups	David Aspinall	2010-08-08
\|
*	proof-allow-undo-in-read-only: remove, use proof-strict-read-only instead.	David Aspinall	2010-08-03
\|
*	proof-full-annotation: default to t; advanced users may turn off.	David Aspinall	2010-08-03
\|
*	Add new option `proof-sticky-errors'.	David Aspinall	2009-11-28
\|
*	proof-strict-read-only: Experimental change to default	David Aspinall	2009-09-14
\|
*	Make quiet by default. Improve docs.	David Aspinall	2009-09-11
\|
*	Default to disabling minibuffer messages	David Aspinall	2009-09-10
\|
*	Add `proof-minibuffer-messages'	David Aspinall	2009-09-10
\|
*	proof-shell-quiet-errors: move to user opts custom group	David Aspinall	2009-09-09
\|
*	proof-allow-undo-in-read-only: change default to nil for new implementation	David Aspinall	2009-09-05
\|
*	Default `proof-full-annotation' to off to cause least surprise to upgraders	David Aspinall	2009-09-05
\|
*	Clean whitespace	David Aspinall	2009-09-05
\|
*	Update docs	David Aspinall	2009-08-31
\|
*	Clean up and rearrange variable declaration files	David Aspinall	2009-08-28