Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | - support Grab Existential Variables for Prooftree | Hendrik Tews | 2013-01-17 | |
| | | | | - protocol change, but stay at version 3 | |||
* | - support bullets and braces in Prooftree | Hendrik Tews | 2013-01-15 | |
| | | | | - prooftree protocol change to version 3 | |||
* | Set version tag for new release. | David Aspinall | 2013-01-11 | |
| | ||||
* | fix parallel overlapping calls of proof-shell-filter | Hendrik Tews | 2013-01-10 | |
| | ||||
* | - fix asserting when parallel background compilation is in progress | Hendrik Tews | 2013-01-03 | |
| | | | | - fix aborting background compilation on error | |||
* | - 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 | |||
* | small typo fixes | Hendrik Tews | 2012-11-13 | |
| | ||||
* | Doc for pg-finish-tracing-display | David Aspinall | 2012-11-09 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-10-19 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-10-19 | |
| | ||||
* | Fixed a bug in three windows mode. | Pierre Courtieu | 2012-09-25 | |
| | ||||
* | Fixed docstring of proof-layout-windows for two columns mode.Was not | Pierre Courtieu | 2012-09-24 | |
| | | | | up-to-date. | |||
* | Fixing a docstring. | Pierre Courtieu | 2012-09-24 | |
| | ||||
* | Completing the possible layouts of proof-layout-windows (added the 3 | Pierre Courtieu | 2012-09-24 | |
| | | | | columns mode). | |||
* | 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 | 2012-09-14 | |
| | | | | to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453 | |||
* | treat #450 by requiring that proofs are started with Proof | Hendrik Tews | 2012-09-12 | |
| | ||||
* | Fixed double hit terminator. Now it is disabled by default, and | Pierre Courtieu | 2012-09-05 | |
| | | | | | | | | 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. | |||
* | Set version tag for new release. | David Aspinall | 2012-09-04 | |
| | ||||
* | Disable HOL Light support for release version | David Aspinall | 2012-09-04 | |
| | ||||
* | Fix header | David Aspinall | 2012-09-02 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-09-02 | |
| | ||||
* | 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 | 2012-08-31 | |
| | | | | 'horizontal 'vertical 'smart policy. | |||
* | Setting nil by default the option to create resp and goals buffer | Pierre Courtieu | 2012-08-31 | |
| | | | | immediately when opening a file. | |||
* | 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-16 | |
| | ||||
* | 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-14 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-08-09 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-07-27 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-07-23 | |
| | ||||
* | Patch to allow byte compilation without X, reported on Gentoo via Ulrich Mueller | David Aspinall | 2012-07-15 | |
| | ||||
* | * generic/pg-user.el (which-func-modes): Fix compiler declaration. | Stefan Monnier | 2012-06-29 | |
| | | | | * generic/proof-site.el (assistants): Fix regexp. | |||
* | Made a small change in generic code about the setting of | Pierre Courtieu | 2012-06-09 | |
| | | | | | | | comment-start-skip: if it is already set then proof-script should not change it. Ultimately if David approves we should moreover fix the setting itself which is bugged. coq-mode now sets this variable by itself. | |||
* | Summary: Handle the new t value of which-func-modes. | Stefan Monnier | 2012-06-08 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-06-05 | |
| | ||||
* | hide cursor in non-selected *goals* and *response* buffers | Hendrik Tews | 2012-06-04 | |
| | ||||
* | let proof-retract-buffer only move point when called interactively | Hendrik Tews | 2012-05-31 | |
| | ||||
* | kill windows showing response and goals buffers on proof-shell-exit | Hendrik Tews | 2012-05-24 | |
| | ||||
* | Use proof-add-to-load-path to extend load-path. This way, | Hendrik Tews | 2012-05-08 | |
| | | | | | distributions with specific requirements (such as Debian with debian-pkg-add-load-path-item) only need to patch one function. | |||
* | Set version tag for new release. | David Aspinall | 2012-04-30 | |
| | ||||
* | enable compilation of generic/proof-autoloads.el | Hendrik Tews | 2012-04-19 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-04-11 | |
| | ||||
* | fix compilation with emacs23-nox of Debian | Hendrik Tews | 2012-03-01 | |
| | ||||
* | proof-shell-start: initialise associated buffers before shell mode, so in ↵ | David Aspinall | 2012-02-08 | |
| | | | | right modes for output from init commands | |||
* | Bump year | David Aspinall | 2012-02-07 | |
| | ||||
* | New pseudo instances to help tool demonstrators in ocaml/ghci (in progress) | David Aspinall | 2012-02-07 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 2012-02-06 | |
| |