aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Collapse)Author
2017-01-19save settings not defined with defpacustom (fixes #142)Hendrik Tews
- infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
2017-01-18split emergency-cleanup to handle interrupts properly (fixes #143)Hendrik Tews
Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors.
2017-01-17move phox from main to obscure instancesHendrik Tews
see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working...
2017-01-17Merge pull request #44 from EasyCrypt/masterhendriktews
EasyCrypt PG mode
2017-01-14Fix prooftree for Coq 8.6Hendrik Tews
In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
2017-01-04Merge remote-tracking branch 'OFFICIAL/master'Pierre Courtieu
2017-01-04Fixing #121 + avoid hiding user windows too much.Pierre Courtieu
2016-12-28fix prooftree crash with long evar linesHendrik Tews
2016-12-14fix generic interrupt procedure to interrupt parallel background compilationHendrik Tews
2016-12-14Merge pull request #129 from hendriktews/keep-goinghendriktews
Keep going
2016-12-14Merge pull request #132 from Matafou/masterPierre Courtieu
Remove default absolute name from coq-prog-name (Fixes #76), but keep displaying…
2016-12-12remove default absolute name from coq-prog-name, but keep dipsplaying it ↵Pierre Courtieu
when asking for it.
2016-12-08option coq-compile-keep-going for parallel compilationHendrik Tews
With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error.
2016-11-30fix 2 compilation warnings (fixes #33)Hendrik Tews
2016-11-02fix error in process filter: Cannot resize windowHendrik Tews
2016-09-25proof-retract-before-change: Fix #41 by saving/restoring the match data.Erik Martin-Dorel
2016-09-19Bump version number for next release cycle.Erik Martin-Dorel
2016-09-18Update the documentation and prepare the release 4.4.Erik Martin-Dorel
2016-09-16Fix reference to log-warning-minimum-levelpsteckler
Fixes #110.
2016-08-25Ensure PG overlays have pg-span property (#98)Tej Chajed
2016-07-04Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta).Erik Martin-Dorel
2016-06-10Reset proof-script-buffer to nil if -ready-prover failsClément Pit--Claudel
Fixes #65
2016-05-24Update PG's logoClément Pit--Claudel
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!
2016-02-13More version number fixesClément Pit--Claudel
2016-01-29Import EasyCrypt PG modePierre-Yves Strub
2016-01-06Merge pull request #22 from ProofGeneral/fix-scrolling-buffersPierre Courtieu
Fix spurious scrolling of *goals* and *response* buffers
2016-01-06Fixing #25.Pierre Courtieu
proof-script-buffer was not set before calling proof-shell-ready-prover.
2015-12-31Fix spurious scrolling of *goals* and *response* buffersClément Pit--Claudel
See https://github.com/cpitclaudel/company-coq/issues/8 and https://github.com/cpitclaudel/company-coq/issues/32 for some background info.
2015-11-13Experimenting less brutal frame deletion.Pierre Courtieu
Only in coq mode for now. There are still some strange frame deletion some times.
2015-11-13Cleaning code for auto width adapting.Pierre Courtieu
Less guessing, separate guessing code.
2015-10-13proof-retract-command-hook added + more auto adjust width in coq mode.Pierre Courtieu
2015-10-12proof-assert-command-hook added + Auto adjust width in coq mode.Pierre Courtieu
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).
2015-10-09Trying to not delete frames too eagerly when laying out.Pierre Courtieu
2015-10-09Fixing 4096 character limit of scomint-send-input.Pierre Courtieu
Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24).
2015-03-13Set version tag for new release.David Aspinall
2015-03-13Summary: Compile warning on speedbar-add-supported-extensionDavid Aspinall
2015-03-13Summary: Fix for bug #489 (make p-electric-terminator-enable appear as minor ↵David Aspinall
mode)
2015-03-11Summary: Update version yearDavid Aspinall
2015-03-09Fixes #503.Pierre Courtieu
Added a "stop silent" if needed in proof-add-queue. This allows to recover verbosity when an error left the prover in silent mode.
2015-02-04cleaned previous commits (generic variable to disable error coloring).Pierre Courtieu
2015-02-02Set version tag for new release.David Aspinall
2015-01-05Set version tag for new release.David Aspinall
2014-12-22Fixed a compilation issue + small display glitch in coqpgPierre Courtieu
2014-12-22Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4.Pierre Courtieu
2014-12-18Fixed 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-06Don'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 newStefan Monnier
display-buffer-alist infrastructure if available.
2013-10-11Set version tag for new release.David Aspinall
2013-07-17Set version tag for new release.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:30:08 +0000