Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fixing #121 + avoid hiding user windows too much. | Pierre Courtieu | 2017-01-04 |
| | |||
* | fix 2 compilation warnings (fixes #33) | Hendrik Tews | 2016-11-30 |
| | |||
* | Ensure PG overlays have pg-span property (#98) | Tej Chajed | 2016-08-25 |
| | |||
* | Experimenting less brutal frame deletion. | Pierre Courtieu | 2015-11-13 |
| | | | | | Only in coq mode for now. There are still some strange frame deletion some times. | ||
* | Cleaning code for auto width adapting. | Pierre Courtieu | 2015-11-13 |
| | | | | Less guessing, separate guessing code. | ||
* | Trying to not delete frames too eagerly when laying out. | Pierre Courtieu | 2015-10-09 |
| | |||
* | Fixed a compilation issue + small display glitch in coqpg | Pierre Courtieu | 2014-12-22 |
| | |||
* | Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4. | Pierre Courtieu | 2014-12-22 |
| | |||
* | Fixed response display spurious newlines for coq. | Pierre Courtieu | 2014-12-18 |
| | | | | | | Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly. | ||
* | * pg-response.el (proof-multiple-frames-enable, proof-next-error): Use new | Stefan Monnier | 2014-06-02 |
| | | | | display-buffer-alist infrastructure if available. | ||
* | Fixed a bug in three windows mode. | Pierre Courtieu | 2012-09-25 |
| | |||
* | Fixed docstring of proof-layout-windows for two columns mode.Was not | Pierre Courtieu | 2012-09-24 |
| | | | | up-to-date. | ||
* | Fixing a docstring. | Pierre Courtieu | 2012-09-24 |
| | |||
* | Completing the possible layouts of proof-layout-windows (added the 3 | Pierre Courtieu | 2012-09-24 |
| | | | | columns mode). | ||
* | Fixed double hit terminator. Now it is disabled by default, and | Pierre Courtieu | 2012-09-05 |
| | | | | | | | | 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. | ||
* | 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 | 2012-08-31 |
| | | | | 'horizontal 'vertical 'smart policy. | ||
* | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | 2012-08-16 |
| | |||
* | hide cursor in non-selected *goals* and *response* buffers | Hendrik Tews | 2012-06-04 |
| | |||
* | Tweak message and display model, in particular, make sure that when a | David Aspinall | 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 handling of trace buffer and tracing slow mode. | David Aspinall | 2011-01-31 |
| | |||
* | Move erase-buffer from associate buffer mode functions, allowing ↵ | David Aspinall | 2010-08-26 |
| | | | | clone-buffer to work, at least superficially. | ||
* | Fixed my last commit where compilation was broken. (function put at | Pierre Courtieu | 2010-08-25 |
| | | | | the wrong place). | ||
* | Fixed the bug of vertical window splitting when the size of the window | Pierre Courtieu | 2010-08-25 |
| | | | | | is too small. However if the frame is too small the bug remains (but it is much less probable). | ||
* | pg-response-has-error-location: save point in response buffer | David Aspinall | 2010-08-17 |
| | |||
* | Checkdoc cleanups | David Aspinall | 2010-08-08 |
| | |||
* | Cleanups for save-excursion to avoid warnings in latest Emacs versions | David Aspinall | 2010-07-08 |
| | |||
* | Keep response and trace buffer read-only, except when changing | David Aspinall | 2009-10-15 |
| | |||
* | proof-display-three-b: avoid giving strange behaviour if some buffers are ↵ | David Aspinall | 2009-09-26 |
| | | | | not available | ||
* | Clean compile | David Aspinall | 2009-09-10 |
| | |||
* | pg-response-display-with-face: remove update of `proof-shell-last-output' | David Aspinall | 2009-09-08 |
| | |||
* | pg-response-maybe-erase: inhibit read only | David Aspinall | 2009-09-06 |
| | |||
* | Clean whitespace | David Aspinall | 2009-09-05 |
| | |||
* | Add proof state hover messages to proof script, along with useful customization. | David Aspinall | 2009-05-26 |
| | |||
* | Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor ↵ | David Aspinall | 2009-05-26 |
| | | | | cleanups | ||
* | Revive sendback behaviour (using button1) | David Aspinall | 2009-05-26 |
| | |||
* | pg-response-display: disable subterm markup removal | David Aspinall | 2008-08-03 |
| | |||
* | Merge changes from Version4Branch. | David Aspinall | 2008-07-24 |
| | |||
* | Revert cursor hide in goals and response to avoid user confusion; use bar ↵ | David Aspinall | 2008-07-05 |
| | | | | cursor. | ||
* | Reduce compiler warnings. Minor fixes. | David Aspinall | 2008-01-16 |
| | |||
* | Compilation tweaks | David Aspinall | 2008-01-16 |
| | |||
* | Revert 8.18: font-lock-append-text-property merges faces better. | David Aspinall | 2008-01-16 |
| | |||
* | pg-response-display: use add-text-properties instead of ↵ | David Aspinall | 2008-01-15 |
| | | | | font-lock-append-text-property [no behaviour change] | ||
* | Many rearrangements for compatibility, efficient/correct compilation, ↵ | David Aspinall | 2008-01-15 |
| | | | | | | | namespaces fixes. pre-shell-start-hook: remove this, use default names for modes proof-compat: simplify architecture flags, use standard (featurep 'xemacs). | ||
* | Use proof-shell-unicode to control whether bytes 128-255 are stripped from ↵ | David Aspinall | 2007-12-14 |
| | | | | output. | ||
* | Emacs compatibility/API updates: string-to-int -> string-to-number | David Aspinall | 2007-12-10 |
| | |||
* | Use button2 instead of button1 for pg-goals-button-action | David Aspinall | 2007-09-06 |
| | |||
* | Only analyse structure for region of appended text | David Aspinall | 2007-08-19 |
| | |||
* | Add support for sending back literal commands reusing PBP markup mechanisms. | David Aspinall | 2007-08-14 |
| | |||
* | Tweaks to buffer history mode. Still intermediate version. | David Aspinall | 2006-09-24 |
| |