Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | merge ProofTreeBranch into main trunk: | 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 | ||
* | Add web style sheet to doc output (work in progress) | 2011-11-09 | |
| | |||
* | Bump doc version numbers to 4.2pre. | 2011-10-14 | |
| | |||
* | Update dates and versions | 2011-10-03 | |
| | |||
* | fix coqdep warning treated as error (library occurring at | 2011-09-23 | |
| | | | | multiple places in load-path) | ||
* | fix doc for coq -R patch | 2011-09-19 | |
| | |||
* | Several improvements: | 2011-09-19 | |
| | | | | | | | | - explain how to use prefix commands for electric terminator as well as C-q - update explanation of locked region and read only options - explain colouring of modeline Scripting indicator - improve document-centred explanation, giving short-cut commands first - correct several uses of main menu "Proof General" to "Proof-General" with hyphen | ||
* | -add support for -R and -I -as in coq-load-path | 2011-09-15 | |
| | | | | -improve documentation (and reorder stuff) | ||
* | Add another contributor. | 2011-09-14 | |
| | |||
* | fix documentation error | 2011-09-09 | |
| | |||
* | Update magic | 2011-08-23 | |
| | |||
* | + fix documentation and one spelling error | 2011-07-05 | |
| | |||
* | Update dates, magic. | 2011-06-10 | |
| | |||
* | Update docstrings | 2011-05-16 | |
| | |||
* | Update docstring magic | 2011-05-12 | |
| | |||
* | Fix emails | 2011-05-05 | |
| | |||
* | Remove mention of dvi | 2011-05-05 | |
| | |||
* | Restore front page scary image. Update dates | 2011-05-05 | |
| | |||
* | Update dates. | 2011-05-05 | |
| | |||
* | Restore scary front page image. Add credits. | 2011-05-05 | |
| | |||
* | Clean up and remove obsolete dvi targets. | 2011-05-05 | |
| | |||
* | Recreate jpg from old front page image (spending some bytes) | 2011-05-05 | |
| | |||
* | - flushed proof-done-advancing-require-function and | 2011-05-05 | |
| | | | | | proof-shell-require-command-regexp - TAGS updated to really flush them | ||
* | Update magic, tweak Makefile to make sure magic uses source .els | 2011-04-26 | |
| | |||
* | Add proof-output-tooltips option to turn off output highlighting for people ↵ | 2011-04-13 | |
| | | | | who read or edit by waving mouse at text | ||
* | typo | 2011-04-12 | |
| | |||
* | - change to proof-restart-buffers for unlocking ancestors | 2011-03-14 | |
| | | | | - improve internal docs for unlocking | ||
* | put coq compilation feature into coq settings menu | 2011-02-14 | |
| | |||
* | - properly display compilation error messages and enable M-x | 2011-02-02 | |
| | | | | next-error (as far as possible) | ||
* | - use low-level compilation interface for external coq | 2011-01-28 | |
| | | | | compilation with our own customization variables | ||
* | - mark new coq specific variables as safe | 2011-01-28 | |
| | | | | - hint on per-directory local variables | ||
* | - more info on the elements of proof-action-list; the COMMANDS | 2011-01-26 | |
| | | | | | list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert. | ||
* | - fix 1 second problem | 2011-01-26 | |
| | | | | - add limitations in the docs | ||
* | Add News for 4.1 | 2011-01-24 | |
| | |||
* | Documentation updates | 2011-01-23 | |
| | |||
* | Update date stamps | 2011-01-19 | |
| | |||
* | - improved doc nodes Using file variables and Locking Ancestors | 2011-01-19 | |
| | |||
* | - implemented coq-lock-ancestors as described in the docs already | 2011-01-18 | |
| | |||
* | - fix broken external compilation | 2011-01-18 | |
| | | | | | | - fix quitting during compilation - substitute "compile" for "recompile" - added documentation | ||
* | - move proof-no-fully-processed-buffer to generic/proof-config | 2011-01-14 | |
| | | | | | | - add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted | ||
* | Tweak text wrt http://proofgeneral.inf.ed.ac.uk/trac/ticket/355 | 2011-01-12 | |
| | |||
* | Whitespace | 2010-10-11 | |
| | |||
* | Add Adam Megacz to credits | 2010-10-11 | |
| | |||
* | Cleanups. | 2010-10-10 | |
| | |||
* | Update magic | 2010-10-10 | |
| | |||
* | Update documenation of mouse bindings. | 2010-10-10 | |
| | | | | | Clean up documentation of holes a bit. Remove some dead comments. | ||
* | Update magic | 2010-10-08 | |
| | |||
* | Improve autosend doc | 2010-10-08 | |
| | |||
* | Fully remove section for Coq-specific variables (coq-version-is-* | 2010-10-04 | |
| | |||
* | Fix some mouse bindings | 2010-10-04 | |
| |