proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
*	Extra test	David Aspinall	2011-12-27
\|
*	Typo	David Aspinall	2011-12-27
\|
*	Fixed some regexp. One for goal closing detection and one for	Pierre Courtieu	2011-12-16
\| \| \| \| \|	understanding the new message about dependent evars (the two window mode was bugged).
*	Adapting coq syntax recognition to the future v8.4 behavior of bullets	Pierre Courtieu	2011-12-16
\| \| \| \| \|	(stand-alone commands), which is different of the experiments made until now in coq/trunk.
*	- protect proof-shell-handle-delayed-output against the case where	Hendrik Tews	2011-12-07
\| \| \| \| \|	proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals
*	ensure optim-resp-window does not change the current buffer	Hendrik Tews	2011-12-06
\|
*	Applied a patch from Tom Prince which makes	Pierre Courtieu	2011-12-05
\| \| \| \|	coq-update-minor-mode-alist behavior more acceptable.
*	Quick stab at support for switching to proof shell when interactive support ↵	David Aspinall	2011-11-15
\| \| \| \|	expected, see Trac #430
*	Small fixes to coq smie indentation.	Pierre Courtieu	2011-11-14
\|
*	Fixed coq smie indentation.	Pierre Courtieu	2011-11-11
\|
*	Fixed coq smie indentation.	Pierre Courtieu	2011-11-10
\|
*	fixed some small bugs in coq indentation smie code.	Pierre Courtieu	2011-11-10
\|
*	added utf8 quantifiers for indentation + small fix in indentation.	Pierre Courtieu	2011-11-08
\|
*	Fixing syntax.	Pierre Courtieu	2011-11-07
\|
*	Fixed a bit more smie coq indentation. Still unfinished but useable.	Pierre Courtieu	2011-11-07
\|
*	Fixed several more bugs in smie indentation code. Not finished.	Pierre Courtieu	2011-11-05
\|
*	slowly fixing the last small bugs in smie indentation.	Pierre Courtieu	2011-11-04
\|
*	Fix previous commit (again).	Pierre Courtieu	2011-11-04
\|
*	Fix previous commit.	Pierre Courtieu	2011-11-04
\|
*	* coq.el (coq-smie-forward-token): Simplify by delegating to backward-token.	Stefan Monnier	2011-11-03
\| \| \| \|	(coq-smie-backward-token): Use memq and member.
*	Fixed the indentation of different kinds of use of the with keyword.	Pierre Courtieu	2011-11-03
\|
*	Added bullet indentation in smie code. smie code still needs some	Pierre Courtieu	2011-11-02
\| \| \| \|	fixing to be be switched on.
*	Attempt to support stricter bytecomp flags	David Aspinall	2011-10-17
\|
*	Update dates and versions	David Aspinall	2011-10-03
\|
*	Move a comment to docstring	David Aspinall	2011-10-03
\|
*	fix coqdep warning treated as error (library occurring at	Hendrik Tews	2011-09-23
\| \| \| \|	multiple places in load-path)
*	fix widget descriptions of coq-load-path	Hendrik Tews	2011-09-15
\|
*	-add support for -R and -I -as in coq-load-path	Hendrik Tews	2011-09-15
\| \| \| \|	-improve documentation (and reorder stuff)
*	fix #421 with solution 1	Hendrik Tews	2011-09-14
\|
*	fix documentation error	Hendrik Tews	2011-09-09
\|
*	Fix trac #420 indentation freezing.	Pierre Courtieu	2011-09-04
\|
*	Non Unicode char	David Aspinall	2011-08-29
\|
*	eval-when-compile -> eval-when (compile) to avoid defvar coq-prog-name	David Aspinall	2011-08-24
\| \| \| \|	overriding setting in coq.el
*	Add back annotation for docstring for texinfo	David Aspinall	2011-08-23
\|
*	Note TODO for indent testing!	David Aspinall	2011-08-23
\|
*	Move coq-prog-name back to coq.el	David Aspinall	2011-08-23
\|
*	Crude patch for Trac #416. I haven't tried to understand indent code fully, ↵	David Aspinall	2011-08-23
\| \| \| \|	so may not be best fix.
*	Fixing track 414 by adding Preterm as a state preserving command.	Pierre Courtieu	2011-07-29
\|
*	Fix compile when smie isnt available	David Aspinall	2011-07-26
\|
*	Fixing the scripting of new subproof script parenthesizing ({ and }).	Pierre Courtieu	2011-07-08
\|
*	+ fix documentation and one spelling error	Hendrik Tews	2011-07-05
\|
*	Some more sample indentation patterns added.	Pierre Courtieu	2011-07-01
\|
*	Remove pointer to closed ticket	David Aspinall	2011-06-22
\|
*	Removed { and } as command terminators for now.	Pierre Courtieu	2011-06-19
\| \| \| \|	Fixes #412.
*	oops, undo last commit.	Pierre Courtieu	2011-06-17
\|
*	Fix mais le find-father ne marche pas encore.	Pierre Courtieu	2011-06-17
\|
*	* coq.el: Fix up a few comment conventions; Improve SMIE indentation.	Stefan Monnier	2011-06-11
\| \| \| \| \| \| \| \| \|	(coq-smie-grammar): Use new special token "Proof End". (coq-smie-proof-end-tokens): New var. (coq-smie-forward-token, coq-smie-backward-token): Map proof end tokens to "Proof End", and map "(Next )Obligation" to "Proof". (coq-smie-rules): Indent after ;-tactical. Use "Proof End". Indent specially "Lemma x :forall, ..".
*	Unplug smie cindentation code for this release.	Pierre Courtieu	2011-06-10
\|
*	Fix trac #410.	Pierre Courtieu	2011-06-10
\|