Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | enable compilation of generic/proof-autoloads.el | 2012-04-19 | |
| | |||
* | Set version tag for new release. | 2012-04-11 | |
| | |||
* | fix compilation with emacs23-nox of Debian | 2012-03-01 | |
| | |||
* | proof-shell-start: initialise associated buffers before shell mode, so in ↵ | 2012-02-08 | |
| | | | | right modes for output from init commands | ||
* | Bump year | 2012-02-07 | |
| | |||
* | New pseudo instances to help tool demonstrators in ocaml/ghci (in progress) | 2012-02-07 | |
| | |||
* | Set version tag for new release. | 2012-02-06 | |
| | |||
* | make sure extra modes available | 2012-01-23 | |
| | |||
* | Typo | 2012-01-19 | |
| | |||
* | lower cpu utilization of splash screen, see Debian bug #642048 | 2012-01-14 | |
| | |||
* | Set version tag for new release. | 2012-01-12 | |
| | |||
* | Set version tag for new release. | 2012-01-10 | |
| | |||
* | Tweak message and display model, in particular, make sure that when a | 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 ↵ | 2012-01-09 | |
| | | | | ignored junk (val it : goalstack =). | ||
* | proof-shell-end-goals-regexp doc: fix inaccuracy, goals always start | 2012-01-09 | |
| | | | | at *start* of proof-shell-start-goals-regexp. | ||
* | Temporarily enable HOL Light globally for testing | 2012-01-05 | |
| | |||
* | * fix case where some existential is instantiated with the last proof command | 2012-01-04 | |
| | | | | | | * protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message | ||
* | Set version tag for new release. | 2012-01-04 | |
| | |||
* | 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 | ||
* | Set version tag for new release. | 2011-12-07 | |
| | |||
* | - protect proof-shell-handle-delayed-output against the case where | 2011-12-07 | |
| | | | | | proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals | ||
* | fix a log of broken customization types | 2011-12-06 | |
| | |||
* | use the start of proof-shell-end-goals-regexp, as documented | 2011-12-06 | |
| | |||
* | Quick stab at support for switching to proof shell when interactive support ↵ | 2011-11-15 | |
| | | | | expected, see Trac #430 | ||
* | Add fix and regression test for Trac #138 | 2011-10-17 | |
| | |||
* | Set version tag for new release. | 2011-10-17 | |
| | |||
* | Attempt to support stricter bytecomp flags | 2011-10-17 | |
| | |||
* | Remove dependency of pg-movie on pg-user | 2011-10-17 | |
| | |||
* | Set version tag for new release. | 2011-10-13 | |
| | |||
* | Patch from Tom Prince to fix Emacs 24 byte compilation (replace ↵ | 2011-10-13 | |
| | | | | interactive-p with called-interactively-p) | ||
* | To fix pgshell mode, restore proof-shell-insert support for a single string ↵ | 2011-10-13 | |
| | | | | argument and allow nil setting for proof-shell-start-goals-regexp. | ||
* | Set version tag for new release. | 2011-10-03 | |
| | |||
* | fix #426 | 2011-09-27 | |
| | |||
* | Set version tag for new release. | 2011-09-19 | |
| | |||
* | proof-full-annotation: default to nil | 2011-09-18 | |
| | |||
* | Set version tag for new release. | 2011-09-16 | |
| | |||
* | fix #421 with solution 1 | 2011-09-14 | |
| | |||
* | proof-electric-terminator: allow a prefix argument to avoid electric action. | 2011-09-14 | |
| | | | | Addresses Trac #422 | ||
* | # User Robin Green <greenrd@greenrd.org> | 2011-09-14 | |
| | | | | Use correct customisation widget for variable-length list of strings | ||
* | Fix typo | 2011-09-14 | |
| | |||
* | Remove contentious call to set-process-query-on-exit-flag, ref Trac#424 | 2011-09-14 | |
| | |||
* | Fix proof-shell-exit optional argument with (interactive) thanks to | 2011-09-11 | |
| | | | | Erik Martin-Dorel. | ||
* | Capitalize menu items | 2011-08-24 | |
| | |||
* | Set version tag for new release. | 2011-08-24 | |
| | |||
* | Remove PG prefix from toolbar button names (needed for disambiguity in older ↵ | 2011-08-23 | |
| | | | | Emacsen, displayed in Emacs 24 UI) | ||
* | Set version tag for new release. | 2011-08-23 | |
| | |||
* | Set version tag for new release. | 2011-06-22 | |
| | |||
* | Set version tag for new release. | 2011-06-22 | |
| | |||
* | Set version tag for new release. | 2011-06-10 | |
| | |||
* | Set version tag for new release. | 2011-06-10 | |
| |