proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
\|
*	Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)	Erik Martin-Dorel	2018-02-20
\| \| \|	Close ProofGeneral/PG#31
*	Remove mmm and ML4PG contribs and remove references to them in code and docs	Paul Steckler	2017-05-24
\|
*	Fix incorrect uses of defvar	Clément Pit--Claudel	2017-03-08
\| \| \| \| \| \| \|	It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance.
*	save settings not defined with defpacustom (fixes #142)	Hendrik Tews	2017-01-19
\| \| \| \| \| \| \|	- infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
*	Fixed a compilation issue + small display glitch in coqpg	Pierre Courtieu	2014-12-22
\|
*	Add option proof-layout-windows-on-visit-file, addressing Trac #444	David Aspinall	2012-08-16
\|
*	merge ProofTreeBranch into main trunk:	Hendrik Tews	2012-01-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof
*	Patch from Tom Prince to fix Emacs 24 byte compilation (replace ↵	David Aspinall	2011-10-13
\| \| \| \|	interactive-p with called-interactively-p)
*	Capitalize menu items	David Aspinall	2011-08-24
\|
*	Remove PG prefix from toolbar button names (needed for disambiguity in older ↵	David Aspinall	2011-08-23
\| \| \| \|	Emacsen, displayed in Emacs 24 UI)
*	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
*	Only make settings commands for dynamic settings which differ from their ↵	David Aspinall	2011-01-31
\| \| \| \|	defaults
*	Make proof-assistant-settings follow currently available dynamic settings, ↵	David Aspinall	2011-01-31
\| \| \| \|	and keep possibly customized variables bound. Closes Trac #387.
*	Improve handling of dynamic preferences. Addresses Trac #387.	David Aspinall	2011-01-31
\|
*	Remove comment	David Aspinall	2011-01-12
\|
*	Add additional support for pgipfloat type	David Aspinall	2011-01-11
\|
*	Patch to add pgipfloat type.	David Aspinall	2010-12-16
\|
*	Move mouse button bindings to avoid clashes (patch from Trac #365, Erik ↵	David Aspinall	2010-10-04
\| \| \| \|	Martin-Dorel)
*	Adjust menu layout for Quick Options. Add Document Centred and Default ↵	David Aspinall	2010-09-21
\| \| \| \|	convenience commands.
*	Implement the eagerly anticipated Beyond Script Management Feature No.2 ↵	David Aspinall	2010-08-27
\| \| \| \|	(i.e., automatic preview of next command)
*	Split proof-assistant-settings-cmds and proof-assistant-settings-cmd	David Aspinall	2010-08-24
\|
*	Use C-c C-H for proof-help as suggested in Trac #341, since C-c h clashes ↵	David Aspinall	2010-08-22
\| \| \| \| \| \|	with holes mode (unfortunately).
*	Move binding of proof-help from C-c C-h to C-c h (see Trac #341)	David Aspinall	2010-08-22
\|
*	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
\|
*	Move key binding for proof assistant keymap (fixes compilation bug)	David Aspinall	2010-08-03
\|
*	Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.	David Aspinall	2010-08-03
\|
*	Rework script span element hiding to avoid buffer-invisibility-spec. Add ↵	David Aspinall	2009-12-03
\| \| \| \|	command elements.
*	Add proof-sticky-errors to quick options menu.	David Aspinall	2009-12-02
\|
*	Remove mention of `proof-script-use-old-parser'.	David Aspinall	2009-12-01
\|
*	proof-splice-separator -> mapconcat builtin	David Aspinall	2009-12-01
\|
*	reverse settings within each group, to prevent upside-down presentation;	Makarius Wenzel	2009-11-24
\|
*	Clean up hints about buffer display	David Aspinall	2009-09-29
\|
*	Menu entry <PA>-set-command invisible when function undefined (not inactive)	David Aspinall	2009-09-28
\|
*	Trace buffer: do not show this trace-output-regexp not set	David Aspinall	2009-09-27
\|
*	Rotate Output Buffers: do not show this if in three window mode	David Aspinall	2009-09-27
\|
*	Follow Upper Case Convention for menu entries	David Aspinall	2009-09-27
\|
*	Tweak hint text	David Aspinall	2009-09-27
\|
*	Put Display submenu first in Quick Options menu	David Aspinall	2009-09-27
\|
*	Shorten menu name	David Aspinall	2009-09-26
\|
*	Add Hide/Show to extra modes menu	David Aspinall	2009-09-21
\|
*	Rearrange options, add customize user options to top level menu	David Aspinall	2009-09-21
\|
*	Adjust comment	David Aspinall	2009-09-14
\|
*	Reorganisation Options with Minor Mode submenu	David Aspinall	2009-09-14
\|
*	Add Read-Only sub menu	David Aspinall	2009-09-11
\|
*	Experimental changes to queue several commands at once and to allow ↵	David Aspinall	2009-09-10
\| \| \| \|	pre-processing of commands when they're queued from script
*	Add proof-minibuffer-messages. Move defpacustom->proof-utils and	David Aspinall	2009-09-10
\| \| \| \|	fix requires.