| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-03 | Process tags in the buffer rather than in strings | Jim Fehrle | |
| 2019-06-01 | Add hook for coq diff-highlighting routine | Jim Fehrle | |
| 2019-05-31 | * coq/coq-diffs.el (coq-insert-tagged-text): Rework to avoid `aset` | Stefan Monnier | |
| (coq-insert-with-face): Don't assume we're at EOB. * generic/pg-goals.el (pg-goals-display): Use with-current-buffer. * generic/pg-response.el (pg-response-maybe-erase): Narrow the scope of inhibit-read-only. (pg-response-display-with-face): Use `member`. Remove unused var `end`. Only bind `start` when we have a value for it. (proof-trace-buffer-display): Use with-current-buffer. | |||
| 2019-05-16 | Highlight diffs in goals and some error messages | Jim Fehrle | |
| using Coq's proof diffs feature. | |||
| 2018-12-12 | Cleanup patch; Moving defvar to toplevel | Stefan Monnier | |
| Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves&restores the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization. | |||
| 2018-08-23 | Fix most doc issues raised by (checkdoc) | Erik Martin-Dorel | |
| 2018-02-21 | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | |
| 2017-03-08 | Remove some Emacs <24.1 compatibility cruft | Clément Pit--Claudel | |
| 2017-01-04 | Fixing #121 + avoid hiding user windows too much. | Pierre Courtieu | |
| 2016-11-30 | fix 2 compilation warnings (fixes #33) | Hendrik Tews | |
| 2016-08-25 | Ensure PG overlays have pg-span property (#98) | Tej Chajed | |
| 2015-11-13 | Experimenting less brutal frame deletion. | Pierre Courtieu | |
| Only in coq mode for now. There are still some strange frame deletion some times. | |||
| 2015-11-13 | Cleaning code for auto width adapting. | Pierre Courtieu | |
| Less guessing, separate guessing code. | |||
| 2015-10-09 | Trying to not delete frames too eagerly when laying out. | Pierre Courtieu | |
| 2014-12-22 | 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-18 | Fixed response display spurious newlines for coq. | Pierre Courtieu | |
| Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly. | |||
| 2014-06-02 | * pg-response.el (proof-multiple-frames-enable, proof-next-error): Use new | Stefan Monnier | |
| display-buffer-alist infrastructure if available. | |||
| 2012-09-25 | Fixed a bug in three windows mode. | Pierre Courtieu | |
| 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-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-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-16 | Add option proof-layout-windows-on-visit-file, addressing Trac #444 | David Aspinall | |
| 2012-06-04 | hide cursor in non-selected *goals* and *response* buffers | Hendrik Tews | |
| 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. | |||
| 2011-01-31 | Improve handling of trace buffer and tracing slow mode. | David Aspinall | |
| 2010-08-26 | Move erase-buffer from associate buffer mode functions, allowing ↵ | David Aspinall | |
| clone-buffer to work, at least superficially. | |||
| 2010-08-25 | Fixed my last commit where compilation was broken. (function put at | Pierre Courtieu | |
| the wrong place). | |||
| 2010-08-25 | Fixed the bug of vertical window splitting when the size of the window | Pierre Courtieu | |
| is too small. However if the frame is too small the bug remains (but it is much less probable). | |||
| 2010-08-17 | pg-response-has-error-location: save point in response buffer | David Aspinall | |
| 2010-08-08 | Checkdoc cleanups | David Aspinall | |
| 2010-07-08 | Cleanups for save-excursion to avoid warnings in latest Emacs versions | David Aspinall | |
| 2009-10-15 | Keep response and trace buffer read-only, except when changing | David Aspinall | |
| 2009-09-26 | proof-display-three-b: avoid giving strange behaviour if some buffers are ↵ | David Aspinall | |
| not available | |||
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-08 | pg-response-display-with-face: remove update of `proof-shell-last-output' | David Aspinall | |
| 2009-09-06 | pg-response-maybe-erase: inhibit read only | David Aspinall | |
| 2009-09-05 | Clean whitespace | David Aspinall | |
| 2009-05-26 | 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 | |
| cleanups | |||
| 2009-05-26 | Revive sendback behaviour (using button1) | David Aspinall | |
| 2008-08-03 | pg-response-display: disable subterm markup removal | David Aspinall | |
| 2008-07-24 | Merge changes from Version4Branch. | David Aspinall | |
| 2008-07-05 | Revert cursor hide in goals and response to avoid user confusion; use bar ↵ | David Aspinall | |
| cursor. | |||
| 2008-01-16 | 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 | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |