| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-09 | Fixes #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-04 | cleaned previous commits (generic variable to disable error coloring). | Pierre Courtieu | |
| 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 ":=". | |||
| 2013-01-15 | - support bullets and braces in Prooftree | Hendrik Tews | |
| - prooftree protocol change to version 3 | |||
| 2013-01-10 | fix parallel overlapping calls of proof-shell-filter | Hendrik Tews | |
| 2013-01-03 | - fix asserting when parallel background compilation is in progress | Hendrik Tews | |
| - fix aborting background compilation on error | |||
| 2012-11-13 | - first version of parallel asynchronous compilation for coq in | Hendrik 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-09 | Doc for pg-finish-tracing-display | David Aspinall | |
| 2012-08-16 | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | |
| 2012-05-24 | kill windows showing response and goals buffers on proof-shell-exit | Hendrik Tews | |
| 2012-02-08 | proof-shell-start: initialise associated buffers before shell mode, so in ↵ | David Aspinall | |
| right modes for output from init commands | |||
| 2012-01-19 | Typo | David Aspinall | |
| 2012-01-10 | Tweak message and display model, in particular, make sure that when a | David Aspinall | |
| 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. | |||
| 2012-01-09 | Improve configuration for HOL Light. Allow goals display to be prefixed by ↵ | David Aspinall | |
| ignored junk (val it : goalstack =). | |||
| 2012-01-03 | merge ProofTreeBranch into main trunk: | Hendrik Tews | |
| - 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 | |||
| 2011-12-07 | - protect proof-shell-handle-delayed-output against the case where | Hendrik Tews | |
| proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals | |||
| 2011-12-06 | use the start of proof-shell-end-goals-regexp, as documented | Hendrik Tews | |
| 2011-11-15 | Quick stab at support for switching to proof shell when interactive support ↵ | David Aspinall | |
| expected, see Trac #430 | |||
| 2011-10-17 | Add fix and regression test for Trac #138 | David Aspinall | |
| 2011-10-13 | To fix pgshell mode, restore proof-shell-insert support for a single string ↵ | David Aspinall | |
| argument and allow nil setting for proof-shell-start-goals-regexp. | |||
| 2011-09-14 | 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-11 | Fix proof-shell-exit optional argument with (interactive) thanks to | Pierre Courtieu | |
| Erik Martin-Dorel. | |||
| 2011-04-19 | * small doc fix | Hendrik Tews | |
| 2011-04-15 | * fix overwriting setq coq-prog-name before loading Proof General | Hendrik Tews | |
| * more complete callback listing in proof-action list doc | |||
| 2011-03-14 | - change to proof-restart-buffers for unlocking ancestors | Hendrik Tews | |
| - improve internal docs for unlocking | |||
| 2011-02-14 | put coq compilation feature into coq settings menu | Hendrik Tews | |
| 2011-01-31 | Improve handling of trace buffer and tracing slow mode. | David Aspinall | |
| 2011-01-26 | - more info on the elements of proof-action-list; the COMMANDS | Hendrik Tews | |
| list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert. | |||
| 2011-01-25 | proof-shell-kill-function: use our own busy loop, as proof-shell-wait | David Aspinall | |
| expects normal prover IO. Addresses http://proofgeneral.inf.ed.ac.uk/trac/ticket/384 | |||
| 2011-01-23 | proof-shell-exit: mention quit command and quit timeout in doc | David Aspinall | |
| 2011-01-23 | Make proof-shell-quit-timeout a prover-specific customize option, default to ↵ | David Aspinall | |
| 45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384. | |||
| 2011-01-23 | Kill prover process without asking on Emacs exit | David Aspinall | |
| 2011-01-18 | - fixed stale load path problem with killing the proof shell in | Hendrik Tews | |
| the deactivation-hook | |||
| 2011-01-18 | Localise compilation fix for dynamic scope of `queueitems\'. | David Aspinall | |
| 2011-01-18 | - fixed compilation errors | Hendrik Tews | |
| 2011-01-18 | - fix broken external compilation | Hendrik Tews | |
| - fix quitting during compilation - substitute "compile" for "recompile" - added documentation | |||
| 2011-01-14 | - simple backward compatible change to invoke a function to | Hendrik Tews | |
| compute the command line arguments for a proof assistant | |||
| 2011-01-12 | Add preliminary support for multiple files for coq. | Hendrik Tews | |
| The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names | |||
| 2010-10-10 | Adjust a comment on proof-shell-mode | David Aspinall | |
| 2010-10-01 | Add explicit 'invisible flag on the action list for invisible commands. | David Aspinall | |
| This means that certain display actions will always be avoided for non-scripting commands (i.e., hints, anything in `proof-shell-error-or-interrupt-hook'). | |||
| 2010-10-01 | proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting ↵ | David Aspinall | |
| input (no non-nil flags in queue) | |||
| 2010-09-29 | Support proof-shell-init-cmd being a list | David Aspinall | |
| 2010-09-29 | Support proof-shell-init-cmd being a list | David Aspinall | |
| 2010-09-21 | Introduce more colourings for active scripting indicator. | David Aspinall | |
| 2010-09-08 | Script mouse face highlighting: new faces/colours for commands and regions, ↵ | David Aspinall | |
| reinstate comment highlighting. | |||
| 2010-08-27 | Replace proof-terminal-char with proof-terminal-string. | David Aspinall | |
| 2010-08-26 | Move erase-buffer from associate buffer mode functions, allowing ↵ | David Aspinall | |
| clone-buffer to work, at least superficially. | |||
| 2010-08-26 | proof-shell-display-output-as-response: fix to check for no-response-display, | David Aspinall | |
| so that proof-shell-invisible-command-invisible-result does what it says on the tin. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |