| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2012-09-24 | Fixed docstring of proof-layout-windows for two columns mode.Was not | Pierre Courtieu | |
| up-to-date. | |||
| 2012-09-24 | Fixing a docstring. | Pierre Courtieu | |
| 2012-09-24 | Completing the possible layouts of proof-layout-windows (added the 3 | Pierre Courtieu | |
| columns mode). | |||
| 2012-09-14 | Set version tag for new release. | David Aspinall | |
| 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-09-12 | treat #450 by requiring that proofs are started with Proof | Hendrik Tews | |
| 2012-09-05 | Fixed double hit terminator. Now it is disabled by default, and | Pierre Courtieu | |
| enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy. | |||
| 2012-09-04 | Set version tag for new release. | David Aspinall | |
| 2012-09-04 | Disable HOL Light support for release version | David Aspinall | |
| 2012-09-02 | Fix header | David Aspinall | |
| 2012-09-02 | Set version tag for new release. | David Aspinall | |
| 2012-08-31 | Three windows mode is back as the default mode. | Pierre Courtieu | |
| 2012-08-31 | Changed the behaviour of proof-layout-windows. Now it follows the | Pierre Courtieu | |
| 'horizontal 'vertical 'smart policy. | |||
| 2012-08-31 | Setting nil by default the option to create resp and goals buffer | Pierre Courtieu | |
| immediately when opening a file. | |||
| 2012-08-16 | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | |
| 2012-08-16 | Better colours on dark frames | David Aspinall | |
| 2012-08-14 | Set version tag for new release. | David Aspinall | |
| 2012-08-14 | Add user option proof-next-command-insert-space. | David Aspinall | |
| 2012-08-14 | fix 443 by enforcing that the prover is not busy in proof-retract-until-point | Hendrik Tews | |
| 2012-08-09 | Set version tag for new release. | David Aspinall | |
| 2012-07-27 | Set version tag for new release. | David Aspinall | |
| 2012-07-23 | Set version tag for new release. | David Aspinall | |
| 2012-07-15 | Patch to allow byte compilation without X, reported on Gentoo via Ulrich Mueller | David Aspinall | |
| 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. | |||
| 2012-06-08 | Summary: Handle the new t value of which-func-modes. | Stefan Monnier | |
| 2012-06-05 | Set version tag for new release. | David Aspinall | |
| 2012-06-04 | hide cursor in non-selected *goals* and *response* buffers | Hendrik Tews | |
| 2012-05-31 | let proof-retract-buffer only move point when called interactively | Hendrik Tews | |
| 2012-05-24 | kill windows showing response and goals buffers on proof-shell-exit | Hendrik Tews | |
| 2012-05-08 | Use proof-add-to-load-path to extend load-path. This way, | Hendrik Tews | |
| distributions with specific requirements (such as Debian with debian-pkg-add-load-path-item) only need to patch one function. | |||
| 2012-04-30 | Set version tag for new release. | David Aspinall | |
| 2012-04-19 | enable compilation of generic/proof-autoloads.el | Hendrik Tews | |
| 2012-04-11 | Set version tag for new release. | David Aspinall | |
| 2012-03-01 | fix compilation with emacs23-nox of Debian | 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-02-07 | Bump year | David Aspinall | |
| 2012-02-07 | New pseudo instances to help tool demonstrators in ocaml/ghci (in progress) | David Aspinall | |
| 2012-02-06 | Set version tag for new release. | David Aspinall | |
| 2012-01-23 | make sure extra modes available | David Aspinall | |
| 2012-01-19 | Typo | David Aspinall | |
| 2012-01-14 | lower cpu utilization of splash screen, see Debian bug #642048 | Hendrik Tews | |
| 2012-01-12 | Set version tag for new release. | David Aspinall | |
| 2012-01-10 | Set version tag for new release. | 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-09 | proof-shell-end-goals-regexp doc: fix inaccuracy, goals always start | David Aspinall | |
| at *start* of proof-shell-start-goals-regexp. | |||
| 2012-01-05 | Temporarily enable HOL Light globally for testing | David Aspinall | |
| 2012-01-04 | * fix case where some existential is instantiated with the last proof command | Hendrik Tews | |
| * protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message | |||
| 2012-01-04 | Set version tag for new release. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |