proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Fix disable evar colorizing in coq file.	Pierre Courtieu	2015-03-27
\|
*	Fixed a regex for detecting ids at point.	Pierre Courtieu	2015-03-27
\|
*	Colorizing hyps names robustified. Still incomplete.	Pierre Courtieu	2015-03-26
\|
*	A command to set coq printing width smartly.	Pierre Courtieu	2015-03-26
\| \| \| \| \|	Set the width to the current goals window. Default binding: C-c C-a C-w.
*	A remark about project file in the documentation.	Pierre Courtieu	2015-03-26
\| \| \| \| \|	Saying that one -arg should be followed by only one option. For several options, put several -arg, ONE PER LINE.
*	Fixed a smal bug in colorizing response buffer.	Pierre Courtieu	2015-03-26
\| \| \| \| \| \|	First constructor of an inductive was colorized as a hyp name. Hyp name colorizing should be done another way. Using font-lock here is probably bad.
*	Fixed indetation of tryif then else.	Pierre Courtieu	2015-03-24
\|
*	fixed gfail hilighting.	Pierre Courtieu	2015-03-24
\|
*	added some keywords	Pierre Courtieu	2015-03-24
\|
*	Highlighting evars.	Pierre Courtieu	2015-03-23
\|
*	Fixed lazymatch and multimatch indentation/highlighting.	Pierre Courtieu	2015-03-23
\|
*	Summary: remove non-BSD cp arg	David Aspinall	2015-03-13
\|
*	Update dates for release next month	David Aspinall	2015-03-13
\|
*	Summary: Experimental Dockerfile	David Aspinall	2015-03-13
\|
*	Set version tag for new release.	David Aspinall	2015-03-13
\|
*	Summary: FAQ about copying output into new buffers	David Aspinall	2015-03-13
\|
*	Summary: Fix to work with dark color themes (stipple with header-line face)	David Aspinall	2015-03-13
\|
*	Summary: Compile warning on speedbar-add-supported-extension	David Aspinall	2015-03-13
\|
*	Summary: Fix for bug #489 (make p-electric-terminator-enable appear as minor ↵	David Aspinall	2015-03-13
\| \| \| \|	mode)
*	Some comments for future work.	Pierre Courtieu	2015-03-13
\|
*	Summary: Revert change to default EMACS	David Aspinall	2015-03-13
\|
*	(fixes last commit) Added a command to send Queries to coq, with completion ↵	Pierre Courtieu	2015-03-13
\| \| \| \| \| \| \|	(C-c C-a C-q). Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag.
*	Added a command to send Queries to coq, with completion (C-c C-a C-q).	Pierre Courtieu	2015-03-13
\| \| \| \| \|	Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag.
*	Summary: Update version year	David Aspinall	2015-03-11
\|
*	Summary: Build in default path for Isabelle2014 Mac package	David Aspinall	2015-03-11
\|
*	Added bug fixes in CHANGES.	Pierre Courtieu	2015-03-09
\|
*	Fixes #503.	Pierre Courtieu	2015-03-09
\| \| \| \| \|	Added a "stop silent" if needed in proof-add-queue. This allows to recover verbosity when an error left the prover in silent mode.
*	Fixed stuff in CHANGES.	Pierre Courtieu	2015-03-05
\|
*	Customization variables for modules, section and proof indentation.	Pierre Courtieu	2015-03-05
\|
*	Summary: Fix compile warning on phox-toolbar-entries	David Aspinall	2015-03-05
\|
*	Summary: Fix compile warning on isar-markup-ml	David Aspinall	2015-03-05
\|
*	Fix compile error with make-face	David Aspinall	2015-03-05
\|
*	Summary: Remove obsolete function	David Aspinall	2015-03-05
\|
*	Summary: Build on Mac	David Aspinall	2015-03-05
\|
*	Fix colours for dark backgrounds	David Aspinall	2015-03-05
\|
*	Fixed Proof end/start detection on Proof using ...	Pierre Courtieu	2015-03-04
\| \| \| \| \|	Was making scripting confused. P.
*	Fixed compilation issue with previous commit + CHANGE updates.	Pierre Courtieu	2015-03-04
\|
*	Mouse queries.	Pierre Courtieu	2015-03-03
\| \| \| \| \|	If enabled, allows to send queries to coq with (control/shift/control-shift) mouse-1.
*	Coqtop always restarted when switching script buffer.	Pierre Courtieu	2015-03-03
\| \| \| \| \| \|	This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options.
*	Making freeze buffer hace coq-response-more.	Pierre Courtieu	2015-02-24
\| \| \| \| \|	So that shortcuts work from this buffer. + colorizing.
*	Typo in last commit.	Pierre Courtieu	2015-02-23
\|
*	Fixed a bug in syntax table making fontlock and indentation fail.	Pierre Courtieu	2015-02-23
\| \| \| \|	After some command detecting things at point, the indentation was broken.
*	Fixed read-only error for compile before require option.	Pierre Courtieu	2015-02-11
\| \| \| \| \| \|	the emacs bug seems solved: the error with read-only always occur whatever locale is used. So I toggle read-only off in coq-compile-response.
*	replug removal of induction principle in SearAbout queries.	Pierre Courtieu	2015-02-09
\|
*	Adding function to grab things at point and send queries about it.	Pierre Courtieu	2015-02-09
\| \| \| \|	No shortcut yet but I am testing some "one click" stuff right now.
*	Removed a debugging message.	Pierre Courtieu	2015-02-06
\|
*	Fix colorization of for coq multiple hypothesis on the same line.	Pierre Courtieu	2015-02-05
\|
*	cleaned previous commits (generic variable to disable error coloring).	Pierre Courtieu	2015-02-04
\|
*	Fixed previous commit (wrong regexp).	Pierre Courtieu	2015-02-04
\|
*	coloring names in resposne and goals	Pierre Courtieu	2015-02-03
\|