| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-04 | cleaned previous commits (generic variable to disable error coloring). | Pierre Courtieu | |
| 2015-02-02 | Set version tag for new release. | David Aspinall | |
| 2015-01-05 | Set version tag for new release. | David Aspinall | |
| 2014-12-22 | Fixed a compilation issue + small display glitch in coqpg | Pierre Courtieu | |
| 2014-12-22 | Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4. | Pierre Courtieu | |
| 2014-12-18 | Fixed response display spurious newlines for coq. | Pierre Courtieu | |
| Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly. | |||
| 2014-06-06 | Don't mess with overlay priorities. | Stefan Monnier | |
| 2014-06-04 | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | Stefan Monnier | |
| (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | |||
| 2014-06-02 | * pg-response.el (proof-multiple-frames-enable, proof-next-error): Use new | Stefan Monnier | |
| display-buffer-alist infrastructure if available. | |||
| 2013-10-11 | Set version tag for new release. | David Aspinall | |
| 2013-07-17 | Set version tag for new release. | David Aspinall | |
| 2013-07-05 | Set version tag for new release. | David Aspinall | |
| 2013-05-22 | rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif} | Hendrik Tews | |
| to fix #472 | |||
| 2013-05-22 | Set version tag for new release. | David Aspinall | |
| 2013-05-10 | Set version tag for new release. | David Aspinall | |
| 2013-03-27 | Set version tag for new release. | David Aspinall | |
| 2013-01-21 | - implement proof-script insertion | Hendrik Tews | |
| 2013-01-20 | - implement retract from prooftree | Hendrik Tews | |
| 2013-01-17 | - support Grab Existential Variables for Prooftree | Hendrik Tews | |
| - protocol change, but stay at version 3 | |||
| 2013-01-15 | - support bullets and braces in Prooftree | Hendrik Tews | |
| - prooftree protocol change to version 3 | |||
| 2013-01-11 | Set version tag for new release. | David Aspinall | |
| 2013-01-10 | fix parallel overlapping calls of proof-shell-filter | Hendrik Tews | |
| 2013-01-03 | - fix asserting when parallel background compilation is in progress | Hendrik Tews | |
| - fix aborting background compilation on error | |||
| 2012-11-13 | - first version of parallel asynchronous compilation for coq in | Hendrik Tews | |
| 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 | |||
| 2012-11-13 | small typo fixes | Hendrik Tews | |
| 2012-11-09 | Doc for pg-finish-tracing-display | David Aspinall | |
| 2012-10-19 | Set version tag for new release. | David Aspinall | |
| 2012-10-19 | Set version tag for new release. | David Aspinall | |
| 2012-09-25 | Fixed a bug in three windows mode. | Pierre Courtieu | |
| 2012-09-24 | Fixed docstring of proof-layout-windows for two columns mode.Was not | Pierre Courtieu | |
| up-to-date. | |||
| 2012-09-24 | Fixing a docstring. | Pierre Courtieu | |
| 2012-09-24 | Completing the possible layouts of proof-layout-windows (added the 3 | Pierre Courtieu | |
| columns mode). | |||
| 2012-09-14 | Set version tag for new release. | David Aspinall | |
| 2012-09-14 | proof-shell-process-connection-type: try using pipes by default in Emacs 24, | David Aspinall | |
| to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453 | |||
| 2012-09-12 | treat #450 by requiring that proofs are started with Proof | Hendrik Tews | |
| 2012-09-05 | Fixed double hit terminator. Now it is disabled by default, and | Pierre Courtieu | |
| enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy. | |||
| 2012-09-04 | Set version tag for new release. | David Aspinall | |
| 2012-09-04 | Disable HOL Light support for release version | David Aspinall | |
| 2012-09-02 | Fix header | David Aspinall | |
| 2012-09-02 | Set version tag for new release. | David Aspinall | |
| 2012-08-31 | 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 | |
| 'horizontal 'vertical 'smart policy. | |||
| 2012-08-31 | Setting nil by default the option to create resp and goals buffer | Pierre Courtieu | |
| immediately when opening a file. | |||
| 2012-08-16 | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | |
| 2012-08-16 | Better colours on dark frames | David Aspinall | |
| 2012-08-14 | Set version tag for new release. | David Aspinall | |
| 2012-08-14 | Add user option proof-next-command-insert-space. | David Aspinall | |
| 2012-08-14 | fix 443 by enforcing that the prover is not busy in proof-retract-until-point | Hendrik Tews | |
| 2012-08-09 | Set version tag for new release. | David Aspinall | |
| 2012-07-27 | Set version tag for new release. | David Aspinall | |
