| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-06-10 | Reset proof-script-buffer to nil if -ready-prover fails | Clément Pit--Claudel | |
| Fixes #65 | |||
| 2016-01-06 | Fixing #25. | Pierre Courtieu | |
| proof-script-buffer was not set before calling proof-shell-ready-prover. | |||
| 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). | |||
| 2014-06-06 | Don't mess with overlay priorities. | Stefan Monnier | |
| 2012-08-16 | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | |
| 2012-08-14 | fix 443 by enforcing that the prover is not busy in proof-retract-until-point | Hendrik Tews | |
| 2012-06-29 | * generic/pg-user.el (which-func-modes): Fix compiler declaration. | Stefan Monnier | |
| * generic/proof-site.el (assistants): Fix regexp. | |||
| 2012-06-09 | Made a small change in generic code about the setting of | Pierre Courtieu | |
| comment-start-skip: if it is already set then proof-script should not change it. Ultimately if David approves we should moreover fix the setting itself which is bugged. coq-mode now sets this variable by itself. | |||
| 2011-10-13 | Patch from Tom Prince to fix Emacs 24 byte compilation (replace ↵ | David Aspinall | |
| interactive-p with called-interactively-p) | |||
| 2011-06-09 | Add autoload. | David Aspinall | |
| 2011-06-08 | - fix for #408: Only use the buffer name in | Hendrik Tews | |
| coq-compile-response-buffer - fix typo elsewhere | |||
| 2011-05-30 | Trac#403: wait for retraction to complete before returning, to | David Aspinall | |
| avoid hitting read only error in calling command. | |||
| 2011-05-27 | ensure (integerp proof-segment-up-to-cache-end), fixes Trac #404 | David Aspinall | |
| 2011-05-26 | proof-retract-before-change: fix Trac #403 (at least partially) by | David Aspinall | |
| removing restriction during automatic retraction so proof-retract-until-point behaves correctly. | |||
| 2011-05-16 | Patch for Trac#400. | David Aspinall | |
| 2011-05-12 | Tweak for `proof-segment-up-to-using-cache': better handling of | David Aspinall | |
| proof-last-edited-low-watermark. | |||
| 2011-05-12 | Attempted fix for `proof-segment-up-to-using-cache', re | David Aspinall | |
| http://proofgeneral.inf.ed.ac.uk/trac/ticket/395 | |||
| 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-26 | Fix for Trac #397. Needs some exercise. | David Aspinall | |
| 2011-04-13 | Add proof-output-tooltips option to turn off output highlighting for people ↵ | David Aspinall | |
| who read or edit by waving mouse at text | |||
| 2011-03-14 | - change to proof-restart-buffers for unlocking ancestors | Hendrik Tews | |
| - improve internal docs for unlocking | |||
| 2011-01-31 | Support mouse action on modeline indicator for scripting mode | David Aspinall | |
| 2011-01-25 | proof-deactivate-scripting: cleanup this function to make more | David Aspinall | |
| intelligible, also to properly support behaviour needed for `proof-no-fully-processed-buffer'. | |||
| 2011-01-24 | - change 'span-delete-action in 'span-delete-actions, which is | Hendrik Tews | |
| now a list of functions to be run when the span is deleted. Use span-add-delete-action to add a delete action. | |||
| 2011-01-23 | proof-protected-process-or-retract: don't give failure error if nothing to do | David Aspinall | |
| Addresses Trac #383 | |||
| 2011-01-19 | pg-show-all-portions: protect against empty hash tables | David Aspinall | |
| 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-10-11 | proof-segment-up-to-using-cache: improve attempt | David Aspinall | |
| 2010-10-10 | Fix debug message format | David Aspinall | |
| 2010-10-10 | pg-span-name: improve docstring. | David Aspinall | |
| proof-complete-buffer-atomic: simplify. Add debug message for parser cache. | |||
| 2010-10-10 | Fix to last patch. | David Aspinall | |
| 2010-10-10 | proof-assert-electric-terminator: prevent adding terminator if point is ↵ | David Aspinall | |
| after it as well as before, as in PG 3.7. Fixes #371. | |||
| 2010-10-01 | Move utility span-make-modifying-removing-span to span.el | David Aspinall | |
| 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-10-01 | Adjust handling of insertion of newlines before next command. | David Aspinall | |
| 2010-09-29 | Doc | David Aspinall | |
| 2010-09-08 | mapcar -> mapc to fix compile error | David Aspinall | |
| 2010-09-08 | Remove debug message | David Aspinall | |
| 2010-09-08 | Improve/fix invisibility management, using buffer-invisibility-spec. Adjust ↵ | David Aspinall | |
| span regions. | |||
| 2010-09-08 | Trivial comment change | David Aspinall | |
| 2010-09-08 | Tidy comments. | David Aspinall | |
| 2010-09-07 | proof-assert-electric-terminator: fix for proof-terminal-string, not char | David Aspinall | |
| 2010-08-27 | Replace proof-terminal-char with proof-terminal-string. | David Aspinall | |
| 2010-08-27 | Implement the eagerly anticipated Beyond Script Management Feature No.2 ↵ | David Aspinall | |
| (i.e., automatic preview of next command) | |||
| 2010-08-25 | Fix compile: declare proof-interrupt-process | David Aspinall | |
| 2010-08-25 | proof-retract-before-change: now interrupts are robust in Isabelle, try | David Aspinall | |
| interrupting if prover is busy before undoing. Refs Trac #293 | |||
| 2010-08-25 | Bring syntactic context functions together | David Aspinall | |
| 2010-08-17 | Autosend: don't autosend after undoing; add proof-shell-last-queuemode to ↵ | David Aspinall | |
| support this. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |