proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Fixing #183.	Pierre Courtieu	2017-05-23
\|
*	Merge pull request #163 from ProofGeneral/fix_indentation	Pierre Courtieu	2017-03-03
\|\ \| \| \| \|	Fix indentation
* \|	use Utf8 from Coq library	Paul Steckler	2017-03-02
\| \|
\| *	Fixing #147 and #91 + others indentation bugs.	Pierre Courtieu	2017-01-26
\|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	While fixing these I discovered several flaws in indentation (what a suprise). The probem is the following: since we don't have a precise grammar of tactics, smie often decides that the parent of a sub-part of a tactic is the previous command instead of the current tacic. Typical example (fixed now but in general): foo. apply bar with bar'. Since "apply ... bar'" is considered as one leaf of the grammar, it is considered to be a child of the previous dot. . /\ / \ foo apply...bar' Therefore indentation of "with" wants to align with parent "." and hence with "foo". Basically we should try to define a much more precise grammar of complex tactics (with with, as, using etc) in order to fix the problem. Of course this has the drawback of making impossible to support user tactic notations.
*	Fixed lazymatch and multimatch indentation/highlighting.	Pierre Courtieu	2015-03-23
\|
*	Fixing indentation of pending curly braces.	Pierre Courtieu	2015-01-05
\|
*	trying to indent pending forall in the expected way	Pierre Courtieu	2015-01-05
\|
*	fixed indentation (lexing of 'with') + made local coq-load-path.	Pierre Courtieu	2014-12-30
\|
*	fixed a bug in command parsing for coq, due to recent changes.	Pierre Courtieu	2014-12-24
\|
*	* coq/coq-smie.el: Fix precedence of 'else'.	Stefan Monnier	2014-06-06
\|
*	* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.	Stefan Monnier	2014-06-04
\| \| \| \| \|	(coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
*	Rename coq-smie-lexer.el to coq-smie.el.	Stefan Monnier	2014-06-03
\|
*	Fixing another bug in indentation concerning "where". Actually there	Pierre Courtieu	2013-07-11
\| \| \| \| \|	are other uses of "where (declaring notation for records that I did no test).
*	- first version of parallel asynchronous compilation for coq in	Hendrik Tews	2012-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used
*	Fixed incorrect syntax of previous commit.	Pierre Courtieu	2012-07-10
\|
*	Indentation is a bit more accurate.	Pierre Courtieu	2012-06-08
\|
*	Fix indentation of dependent match clauses (as ... in ... return ...).	Pierre Courtieu	2012-06-07
\| \| \| \|	+ bug fixes.
*	One more fix for indentation.	Pierre Courtieu	2012-06-04
\|
*	Fix a bug of indentation.	Pierre Courtieu	2012-06-03
\|
*	fix typo + add one missing cvsignore	Hendrik Tews	2012-05-09
\|
*	Fixed an ineficiency in comment detection.	Pierre Courtieu	2012-02-10
\|
*	Typo	David Aspinall	2011-12-27
\|
*	Fixing the scripting of new subproof script parenthesizing ({ and }).	Pierre Courtieu	2011-07-08
\|
*	Some more sample indentation patterns added.	Pierre Courtieu	2011-07-01
\|
*	oops, undo last commit.	Pierre Courtieu	2011-06-17
\|
*	Fix trac #410.	Pierre Courtieu	2011-06-10
\|
*	Added one indentation example.	Pierre Courtieu	2011-06-08
\|
*	Updated the old code for indentation, in case Stefan cannot finish the	Pierre Courtieu	2011-06-04
\| \| \| \| \| \| \|	new one for the release. Added also support for an experimental syntax modification: { .. } is a new syntax for Beginsubproof. ... EndSubproof. There a also few minor behavior changes. The code has changed a lot though.
*	- minor changes: clean personal todo list + adjust test case description	Hendrik Tews	2011-05-20
\|
*	- add test coq/ex/test-cases/change-ancestor for the	Hendrik Tews	2011-05-12
\| \| \| \|	change-ancestor bug
*	- adjust coq-ask-insert-coq-prog-name and doc in coq-local-vars-doc	Hendrik Tews	2011-02-28
\|
*	- fix problem description	Hendrik Tews	2011-01-26
\|
*	- use time-less-p	Hendrik Tews	2011-01-21
\| \| \| \| \| \| \|	- delete previous-head, simplify loop - coq 8.2 compatibility - describe bug for killing completely asserted active buffers in coq/ex/test-cases/retract-completely-asserted
*	- fixed stale load path problem with killing the proof shell in	Hendrik Tews	2011-01-18
\| \| \| \|	the deactivation-hook
*	fix problems in test cases	Hendrik Tews	2011-01-17
\| \| \| \|	coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir
*	- more coq test cases (some with surprising and embarrassing bugs)	Hendrik Tews	2011-01-14
\|
*	- 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
*	Fixed small bugs in indentation.	Pierre Courtieu	2010-09-09
\|
*	illustrating the wrongness of the current multifile processing for coq.	Pierre Courtieu	2010-09-08
\|
*	Added three files for testing multi file scripting.	Pierre Courtieu	2010-09-08
\|
*	Moved files	David Aspinall	2010-08-15
\|
*	Renamed file	David Aspinall	2010-08-13