Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | More version number fixes | 2016-02-13 | ||
| | | ||||
| * | Import EasyCrypt PG mode | 2016-01-29 | ||
|/ | ||||
* | Merge pull request #22 from ProofGeneral/fix-scrolling-buffers | 2016-01-06 | ||
|\ | | | | | Fix spurious scrolling of *goals* and *response* buffers | |||
* | | Fixing #25. | 2016-01-06 | ||
| | | | | | | | | proof-script-buffer was not set before calling proof-shell-ready-prover. | |||
| * | Fix spurious scrolling of *goals* and *response* buffers | 2015-12-31 | ||
|/ | | | | | | See https://github.com/cpitclaudel/company-coq/issues/8 and https://github.com/cpitclaudel/company-coq/issues/32 for some background info. | |||
* | Experimenting less brutal frame deletion. | 2015-11-13 | ||
| | | | | | Only in coq mode for now. There are still some strange frame deletion some times. | |||
* | Cleaning code for auto width adapting. | 2015-11-13 | ||
| | | | | Less guessing, separate guessing code. | |||
* | proof-retract-command-hook added + more auto adjust width in coq mode. | 2015-10-13 | ||
| | ||||
* | proof-assert-command-hook added + Auto adjust width in coq mode. | 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. | 2015-10-09 | ||
| | ||||
* | Fixing 4096 character limit of scomint-send-input. | 2015-10-09 | ||
| | | | | | Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24). | |||
* | Set version tag for new release. | 2015-03-13 | ||
| | ||||
* | Summary: Compile warning on speedbar-add-supported-extension | 2015-03-13 | ||
| | ||||
* | Summary: Fix for bug #489 (make p-electric-terminator-enable appear as minor ↵ | 2015-03-13 | ||
| | | | | mode) | |||
* | Summary: Update version year | 2015-03-11 | ||
| | ||||
* | Fixes #503. | 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). | 2015-02-04 | ||
| | ||||
* | Set version tag for new release. | 2015-02-02 | ||
| | ||||
* | Set version tag for new release. | 2015-01-05 | ||
| | ||||
* | Fixed a compilation issue + small display glitch in coqpg | 2014-12-22 | ||
| | ||||
* | Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4. | 2014-12-22 | ||
| | ||||
* | Fixed response display spurious newlines for coq. | 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. | 2014-06-06 | ||
| | ||||
* | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | 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 | 2014-06-02 | ||
| | | | | display-buffer-alist infrastructure if available. | |||
* | Set version tag for new release. | 2013-10-11 | ||
| | ||||
* | Set version tag for new release. | 2013-07-17 | ||
| | ||||
* | Set version tag for new release. | 2013-07-05 | ||
| | ||||
* | rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif} | 2013-05-22 | ||
| | | | | to fix #472 | |||
* | Set version tag for new release. | 2013-05-22 | ||
| | ||||
* | Set version tag for new release. | 2013-05-10 | ||
| | ||||
* | Set version tag for new release. | 2013-03-27 | ||
| | ||||
* | - implement proof-script insertion | 2013-01-21 | ||
| | ||||
* | - implement retract from prooftree | 2013-01-20 | ||
| | ||||
* | - support Grab Existential Variables for Prooftree | 2013-01-17 | ||
| | | | | - protocol change, but stay at version 3 | |||
* | - support bullets and braces in Prooftree | 2013-01-15 | ||
| | | | | - prooftree protocol change to version 3 | |||
* | Set version tag for new release. | 2013-01-11 | ||
| | ||||
* | fix parallel overlapping calls of proof-shell-filter | 2013-01-10 | ||
| | ||||
* | - fix asserting when parallel background compilation is in progress | 2013-01-03 | ||
| | | | | - fix aborting background compilation on error | |||
* | - first version of parallel asynchronous compilation for coq in | 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 | 2012-11-13 | ||
| | ||||
* | Doc for pg-finish-tracing-display | 2012-11-09 | ||
| | ||||
* | Set version tag for new release. | 2012-10-19 | ||
| | ||||
* | Set version tag for new release. | 2012-10-19 | ||
| | ||||
* | Fixed a bug in three windows mode. | 2012-09-25 | ||
| | ||||
* | Fixed docstring of proof-layout-windows for two columns mode.Was not | 2012-09-24 | ||
| | | | | up-to-date. | |||
* | Fixing a docstring. | 2012-09-24 | ||
| | ||||
* | Completing the possible layouts of proof-layout-windows (added the 3 | 2012-09-24 | ||
| | | | | columns mode). | |||
* | Set version tag for new release. | 2012-09-14 | ||
| | ||||
* | proof-shell-process-connection-type: try using pipes by default in Emacs 24, | 2012-09-14 | ||
| | | | | to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453 |