Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Experimenting less brutal frame deletion. | Pierre Courtieu | 2015-11-13 |
| | | | | | Only in coq mode for now. There are still some strange frame deletion some times. | ||
* | Cleaning code for auto width adapting. | Pierre Courtieu | 2015-11-13 |
| | | | | Less guessing, separate guessing code. | ||
* | proof-retract-command-hook added + more auto adjust width in coq mode. | Pierre Courtieu | 2015-10-13 |
| | |||
* | proof-assert-command-hook added + Auto adjust width in coq mode. | Pierre Courtieu | 2015-10-12 |
| | | | | | | | This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing). | ||
* | Trying to not delete frames too eagerly when laying out. | Pierre Courtieu | 2015-10-09 |
| | |||
* | Fixing 4096 character limit of scomint-send-input. | Pierre Courtieu | 2015-10-09 |
| | | | | | Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24). | ||
* | Set version tag for new release. | 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) | ||
* | Summary: Update version year | David Aspinall | 2015-03-11 |
| | |||
* | 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. | ||
* | cleaned previous commits (generic variable to disable error coloring). | Pierre Courtieu | 2015-02-04 |
| | |||
* | Set version tag for new release. | David Aspinall | 2015-02-02 |
| | |||
* | Set version tag for new release. | David Aspinall | 2015-01-05 |
| | |||
* | 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-22 |
| | |||
* | Fixed response display spurious newlines for coq. | Pierre Courtieu | 2014-12-18 |
| | | | | | | Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly. | ||
* | Don't mess with overlay priorities. | 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 ":=". | ||
* | * pg-response.el (proof-multiple-frames-enable, proof-next-error): Use new | Stefan Monnier | 2014-06-02 |
| | | | | display-buffer-alist infrastructure if available. | ||
* | Set version tag for new release. | David Aspinall | 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 |
| | |||
* | rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif} | Hendrik Tews | 2013-05-22 |
| | | | | to fix #472 | ||
* | Set version tag for new release. | David Aspinall | 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 |
| | |||
* | - implement proof-script insertion | Hendrik Tews | 2013-01-21 |
| | |||
* | - implement retract from prooftree | Hendrik Tews | 2013-01-20 |
| | |||
* | - 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 |
| |