Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | fix prooftree crash with long evar lines | Hendrik Tews | 2016-12-28 | |
| | | | ||||
| * | | fix generic interrupt procedure to interrupt parallel background compilation | Hendrik Tews | 2016-12-14 | |
| | | | ||||
| * | | Merge pull request #129 from hendriktews/keep-going | hendriktews | 2016-12-14 | |
|/| | | | | | | | | Keep going | |||
* | | | Merge pull request #132 from Matafou/master | Pierre Courtieu | 2016-12-14 | |
|\ \ \ | | | | | | | | | Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying… | |||
| * | | | remove default absolute name from coq-prog-name, but keep dipsplaying it ↵ | Pierre Courtieu | 2016-12-12 | |
| | | | | | | | | | | | | | | | | when asking for it. | |||
| | * | | option coq-compile-keep-going for parallel compilation | Hendrik Tews | 2016-12-08 | |
| |/ / |/| | | | | | | | | | | | | | | With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error. | |||
* | | | fix 2 compilation warnings (fixes #33) | Hendrik Tews | 2016-11-30 | |
|/ / | ||||
* | | fix error in process filter: Cannot resize window | Hendrik Tews | 2016-11-02 | |
| | | ||||
* | | proof-retract-before-change: Fix #41 by saving/restoring the match data. | Erik Martin-Dorel | 2016-09-25 | |
| | | ||||
* | | Bump version number for next release cycle. | Erik Martin-Dorel | 2016-09-19 | |
| | | ||||
* | | Update the documentation and prepare the release 4.4. | Erik Martin-Dorel | 2016-09-18 | |
| | | ||||
* | | Fix reference to log-warning-minimum-level | psteckler | 2016-09-16 | |
| | | | | | | Fixes #110. | |||
* | | Ensure PG overlays have pg-span property (#98) | Tej Chajed | 2016-08-25 | |
| | | ||||
* | | Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta). | Erik Martin-Dorel | 2016-07-04 | |
| | | ||||
* | | Reset proof-script-buffer to nil if -ready-prover fails | Clément Pit--Claudel | 2016-06-10 | |
| | | | | | | | | Fixes #65 | |||
* | | Update PG's logo | Clément Pit--Claudel | 2016-05-24 | |
| | | | | | | | | | | | | | | The new art is a contribution of Yoshihiro Imai (http://proofcafe.org/~yoshihiro503/), first released at https://github.com/yoshihiro503/generaltan and kindly made available under the terms of the GPL. Many thanks! | |||
* | | More version number fixes | Clément Pit--Claudel | 2016-02-13 | |
| | | ||||
| * | Import EasyCrypt PG mode | Pierre-Yves Strub | 2016-01-29 | |
|/ | ||||
* | Merge pull request #22 from ProofGeneral/fix-scrolling-buffers | Pierre Courtieu | 2016-01-06 | |
|\ | | | | | Fix spurious scrolling of *goals* and *response* buffers | |||
* | | Fixing #25. | Pierre Courtieu | 2016-01-06 | |
| | | | | | | | | proof-script-buffer was not set before calling proof-shell-ready-prover. | |||
| * | Fix spurious scrolling of *goals* and *response* buffers | Clément Pit--Claudel | 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. | 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 | |
| |