aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Collapse)Author
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
2013-07-05Set version tag for new release.David Aspinall
2013-05-22rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif}Hendrik Tews
to fix #472
2013-05-22Set version tag for new release.David Aspinall
2013-05-10Set version tag for new release.David Aspinall
2013-03-27Set version tag for new release.David Aspinall
2013-01-21- implement proof-script insertionHendrik Tews
2013-01-20- implement retract from prooftreeHendrik Tews
2013-01-17- support Grab Existential Variables for ProoftreeHendrik Tews
- protocol change, but stay at version 3
2013-01-15- support bullets and braces in ProoftreeHendrik Tews
- prooftree protocol change to version 3
2013-01-11Set version tag for new release.David Aspinall
2013-01-10fix parallel overlapping calls of proof-shell-filterHendrik Tews
2013-01-03- fix asserting when parallel background compilation is in progressHendrik Tews
- fix aborting background compilation on error
2012-11-13- first version of parallel asynchronous compilation for coq inHendrik Tews
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
2012-11-13small typo fixesHendrik Tews
2012-11-09Doc for pg-finish-tracing-displayDavid Aspinall
2012-10-19Set version tag for new release.David Aspinall
2012-10-19Set version tag for new release.David Aspinall
2012-09-25Fixed a bug in three windows mode.Pierre Courtieu
2012-09-24Fixed docstring of proof-layout-windows for two columns mode.Was notPierre Courtieu
up-to-date.
2012-09-24Fixing a docstring.Pierre Courtieu
2012-09-24Completing the possible layouts of proof-layout-windows (added the 3Pierre Courtieu
columns mode).
2012-09-14Set version tag for new release.David Aspinall
2012-09-14proof-shell-process-connection-type: try using pipes by default in Emacs 24,David Aspinall
to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453
2012-09-12treat #450 by requiring that proofs are started with ProofHendrik Tews
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:39:23 +0000