| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix most doc issues raised by (checkdoc) |  Erik Martin-Dorel | 2018-08-23 |
| | | |||
| * | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | 2018-02-21 |
| | | |||
| * | Fixing bug #187 by removing trailing spaces from prog name. |  Pierre Courtieu | 2017-06-06 |
| | | |||
| * | Change (eval-when (compile) ...) to (eval-when-compile ...) |  Clément Pit--Claudel | 2017-05-05 |
| | | | | | This fixes a bunch of compilation warnings | ||
| * | Merge pull request #157 from ProofGeneral/elpa |  Clément Pit-Claudel | 2017-05-05 |
| |\ | | | | | [WIP] ELPA/MELPA support | ||
| * | | Fixing #167. | Pierre Courtieu | 2017-03-13 |
| | | | |||
| | * | Remove unnecessary calls to 'eval-and-compile' | Clément Pit--Claudel | 2017-03-08 |
| |/ | |||
| * | Removing spurious debug messages. | Pierre Courtieu | 2017-02-24 |
| | | |||
| * | Fixing #154. | Pierre Courtieu | 2017-02-23 |
| | | |||
| * | split emergency-cleanup to handle interrupts properly (fixes #143) |  Hendrik Tews | 2017-01-18 |
| | | | | | | | Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors. | ||
| * | 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 |
| |/ | |||
| * | Reset proof-script-buffer to nil if -ready-prover fails | Clément Pit--Claudel | 2016-06-10 |
| | | | | | Fixes #65 | ||
| * | 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. | ||
| * | Trying to not delete frames too eagerly when laying out. | Pierre Courtieu | 2015-10-09 |
| | | |||
| * | 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 |
| | | |||
| * | * 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 ":=". | ||
| * | - support bullets and braces in Prooftree | Hendrik Tews | 2013-01-15 |
| | | | | | - prooftree protocol change to version 3 | ||
| * | 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 | ||
| * | Doc for pg-finish-tracing-display |  David Aspinall | 2012-11-09 |
| | | |||
| * | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | 2012-08-16 |
| | | |||
| * | kill windows showing response and goals buffers on proof-shell-exit | Hendrik Tews | 2012-05-24 |
| | | |||
| * | proof-shell-start: initialise associated buffers before shell mode, so in ↵ | David Aspinall | 2012-02-08 |
| | | | | | right modes for output from init commands | ||
| * | Typo | David Aspinall | 2012-01-19 |
| | | |||
| * | Tweak message and display model, in particular, make sure that when a | David Aspinall | 2012-01-10 |
| | | | | | | | | | | | | | | | | | response appears above a goals output, the goals output is displayed second, so it is the one that remains visible to the user in the default 2-pane mode. This works with output like this in HOL Light: Warning: Free variables in goal: A, B val it : goalstack = 1 subgoal (1 total) ... and similar cases in Isabelle and Coq. The fix involves some ugly messing with the flags for clearing the response buffer (see `pg-response-maybe-erase'). This could surely be streamlined. | ||
| * | Improve configuration for HOL Light. Allow goals display to be prefixed by ↵ | David Aspinall | 2012-01-09 |
| | | | | | ignored junk (val it : goalstack =). | ||
| * | merge ProofTreeBranch into main trunk: | Hendrik Tews | 2012-01-03 |
| | | | | | | | | | | | | | | | | | - add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof | ||
| * | - protect proof-shell-handle-delayed-output against the case where | Hendrik Tews | 2011-12-07 |
| | | | | | | proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals | ||
| * | use the start of proof-shell-end-goals-regexp, as documented | Hendrik Tews | 2011-12-06 |
| | | |||
| * | Quick stab at support for switching to proof shell when interactive support ↵ | David Aspinall | 2011-11-15 |
| | | | | | expected, see Trac #430 | ||
| * | Add fix and regression test for Trac #138 | David Aspinall | 2011-10-17 |
| | | |||
| * | To fix pgshell mode, restore proof-shell-insert support for a single string ↵ | David Aspinall | 2011-10-13 |
| | | | | | argument and allow nil setting for proof-shell-start-goals-regexp. | ||
| * | fix #421 with solution 1 | Hendrik Tews | 2011-09-14 |
| | | |||
| * | Fix typo | David Aspinall | 2011-09-14 |
| | | |||
| * | Remove contentious call to set-process-query-on-exit-flag, ref Trac#424 | David Aspinall | 2011-09-14 |
| | | |||
| * | Fix proof-shell-exit optional argument with (interactive) thanks to | Pierre Courtieu | 2011-09-11 |
| | | | | | Erik Martin-Dorel. | ||
| * | * small doc fix | Hendrik Tews | 2011-04-19 |
| | | |||
| * | * fix overwriting setq coq-prog-name before loading Proof General | Hendrik Tews | 2011-04-15 |
| | | | | | * more complete callback listing in proof-action list doc | ||
| * | - change to proof-restart-buffers for unlocking ancestors | Hendrik Tews | 2011-03-14 |
| | | | | | - improve internal docs for unlocking | ||
| * | put coq compilation feature into coq settings menu | Hendrik Tews | 2011-02-14 |
| | | |||
| * | Improve handling of trace buffer and tracing slow mode. | David Aspinall | 2011-01-31 |
| | | |||
| * | - more info on the elements of proof-action-list; the COMMANDS | Hendrik Tews | 2011-01-26 |
| | | | | | | list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert. | ||
| * | proof-shell-kill-function: use our own busy loop, as proof-shell-wait | David Aspinall | 2011-01-25 |
| | | | | | | expects normal prover IO. Addresses http://proofgeneral.inf.ed.ac.uk/trac/ticket/384 | ||
 |
index : proof-general | |
| Emacs interface for proof assistants |
| aboutsummaryrefslogtreecommitdiffhomepage |