| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-12-14 | fix generic interrupt procedure to interrupt parallel background compilation | Hendrik Tews | |
| 2015-10-13 | proof-retract-command-hook added + more auto adjust width in coq mode. | Pierre Courtieu | |
| 2015-10-12 | proof-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-09 | Fixing 4096 character limit of scomint-send-input. | Pierre Courtieu | |
| Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24). | |||
| 2015-02-04 | cleaned previous commits (generic variable to disable error coloring). | Pierre Courtieu | |
| 2014-12-18 | Fixed response display spurious newlines for coq. | Pierre Courtieu | |
| Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly. | |||
| 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-09-14 | proof-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-01-09 | Improve configuration for HOL Light. Allow goals display to be prefixed by ↵ | David Aspinall | |
| ignored junk (val it : goalstack =). | |||
| 2012-01-09 | proof-shell-end-goals-regexp doc: fix inaccuracy, goals always start | David Aspinall | |
| at *start* of proof-shell-start-goals-regexp. | |||
| 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-06 | fix a log of broken customization types | 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-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-05-05 | - flushed proof-done-advancing-require-function and | Hendrik Tews | |
| proof-shell-require-command-regexp - TAGS updated to really flush them | |||
| 2011-04-13 | proof-shell-insert-hook: Clean docstring, addressing #396. | 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 | Fix typo | David Aspinall | |
| 2011-01-18 | - fixed compilation errors | Hendrik Tews | |
| 2011-01-14 | - move proof-no-fully-processed-buffer to generic/proof-config | Hendrik Tews | |
| - add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted | |||
| 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-12-16 | Patch to add pgipfloat type. | David Aspinall | |
| 2010-09-29 | Support proof-shell-init-cmd being a list | David Aspinall | |
| 2010-08-27 | Replace proof-terminal-char with proof-terminal-string. | David Aspinall | |
| 2010-08-24 | Reduce quit timeout to sensible value | David Aspinall | |
| 2010-08-19 | proof-shell-process-connection-type: Revert to long-lived previous default ↵ | David Aspinall | |
| of t (for safety, no ill behaviour observed) | |||
| 2010-08-18 | proof-shell-process-connection-type: remove near obsolete test and text | David Aspinall | |
| about Solaris. Experiment using pipe instead of pty communication as default now scomint buffer not intended for interactive input and runs prover process directly. | |||
| 2010-08-17 | Clean up handling of pending interrupts, remove experimental ↵ | David Aspinall | |
| proof-shell-interrupts-after-commit. | |||
| 2010-08-15 | proof-shell-interrupts-after-commit: support commit-before-interrupt mode ↵ | David Aspinall | |
| [experimental/temporary]. | |||
| 2010-08-08 | Checkdoc cleanups | David Aspinall | |
| 2009-12-04 | docstring | David Aspinall | |
| 2009-11-30 | Replace proof-locked-end -> proof-unprocessed-begin | David Aspinall | |
| 2009-11-30 | even higher proof-shell-quit-timeout -- saving main HOL takes 20s on a ↵ | Makarius Wenzel | |
| *fast* machine; | |||
| 2009-11-29 | raised proof-shell-quit-timeout to accomodate bulky write-back images; | Makarius Wenzel | |
| 2009-11-28 | Remove doc mention of obsolete function `pg-assoc-analyse-structure'. | David Aspinall | |
| 2009-10-15 | proof-script-use-old-parser: remove configuration option and cleanup | David Aspinall | |
| 2009-10-14 | Remove `next-entity' settings for func-menu. | David Aspinall | |
| 2009-09-28 | Typo | David Aspinall | |
| 2009-09-28 | Functions find-and-forget and count-undos now return lists of commands | David Aspinall | |
| 2009-09-11 | Fix docs | David Aspinall | |
| 2009-09-10 | Experimental changes to queue several commands at once and to allow ↵ | David Aspinall | |
| pre-processing of commands when they're queued from script | |||
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-09 | Add proof-shell-font-lock-keywords, proof-arbitrary-undo-positions | David Aspinall | |
| 2009-09-09 | p-s-classify-output -> p-s-handle-output, and simplify system-specific hook | David Aspinall | |
| 2009-09-09 | proof-shell-quiet-errors: move to user opts custom group | David Aspinall | |
| 2009-09-08 | proof-kill-goal-command: default to nil, not empty string | David Aspinall | |
| 2009-09-08 | Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵ | David Aspinall | |
| LEGO messages) | |||
| 2009-09-08 | Fix docstrings, remove spurious null | David Aspinall | |
| 2009-09-06 | Change type of proof-shell-process-file, proof-shell-compute-new-files-list | David Aspinall | |
| 2009-09-06 | Clarify that eager message matches are now anchored | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |