aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-response.el
Commit message (Collapse)AuthorAge
* Cleanup patch; Moving defvar to toplevelGravatar Stefan Monnier2018-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
|
* Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
|
* Remove some Emacs <24.1 compatibility cruftGravatar Clément Pit--Claudel2017-03-08
|
* Fixing #121 + avoid hiding user windows too much.Gravatar Pierre Courtieu2017-01-04
|
* fix 2 compilation warnings (fixes #33)Gravatar Hendrik Tews2016-11-30
|
* Ensure PG overlays have pg-span property (#98)Gravatar Tej Chajed2016-08-25
|
* Experimenting less brutal frame deletion.Gravatar Pierre Courtieu2015-11-13
| | | | | Only in coq mode for now. There are still some strange frame deletion some times.
* Cleaning code for auto width adapting.Gravatar Pierre Courtieu2015-11-13
| | | | Less guessing, separate guessing code.
* Trying to not delete frames too eagerly when laying out.Gravatar Pierre Courtieu2015-10-09
|
* Fixed a compilation issue + small display glitch in coqpgGravatar Pierre Courtieu2014-12-22
|
* Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4.Gravatar Pierre Courtieu2014-12-22
|
* Fixed response display spurious newlines for coq.Gravatar Pierre Courtieu2014-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 newGravatar Stefan Monnier2014-06-02
| | | | display-buffer-alist infrastructure if available.
* Fixed a bug in three windows mode.Gravatar Pierre Courtieu2012-09-25
|
* Fixed docstring of proof-layout-windows for two columns mode.Was notGravatar Pierre Courtieu2012-09-24
| | | | up-to-date.
* Fixing a docstring.Gravatar Pierre Courtieu2012-09-24
|
* Completing the possible layouts of proof-layout-windows (added the 3Gravatar Pierre Courtieu2012-09-24
| | | | columns mode).
* Fixed double hit terminator. Now it is disabled by default, andGravatar Pierre Courtieu2012-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.Gravatar Pierre Courtieu2012-08-31
|
* Changed the behaviour of proof-layout-windows. Now it follows theGravatar Pierre Courtieu2012-08-31
| | | | 'horizontal 'vertical 'smart policy.
* Add option proof-layout-windows-on-visit-file, addressing Trac #444Gravatar David Aspinall2012-08-16
|
* hide cursor in non-selected *goals* and *response* buffersGravatar Hendrik Tews2012-06-04
|
* Tweak message and display model, in particular, make sure that when aGravatar David Aspinall2012-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.Gravatar David Aspinall2011-01-31
|
* Move erase-buffer from associate buffer mode functions, allowing ↵Gravatar David Aspinall2010-08-26
| | | | clone-buffer to work, at least superficially.
* Fixed my last commit where compilation was broken. (function put atGravatar Pierre Courtieu2010-08-25
| | | | the wrong place).
* Fixed the bug of vertical window splitting when the size of the windowGravatar Pierre Courtieu2010-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 bufferGravatar David Aspinall2010-08-17
|
* Checkdoc cleanupsGravatar David Aspinall2010-08-08
|
* Cleanups for save-excursion to avoid warnings in latest Emacs versionsGravatar David Aspinall2010-07-08
|
* Keep response and trace buffer read-only, except when changingGravatar David Aspinall2009-10-15
|
* proof-display-three-b: avoid giving strange behaviour if some buffers are ↵Gravatar David Aspinall2009-09-26
| | | | not available
* Clean compileGravatar David Aspinall2009-09-10
|
* pg-response-display-with-face: remove update of `proof-shell-last-output'Gravatar David Aspinall2009-09-08
|
* pg-response-maybe-erase: inhibit read onlyGravatar David Aspinall2009-09-06
|
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* Add proof state hover messages to proof script, along with useful customization.Gravatar David Aspinall2009-05-26
|
* Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor ↵Gravatar David Aspinall2009-05-26
| | | | cleanups
* Revive sendback behaviour (using button1)Gravatar David Aspinall2009-05-26
|
* pg-response-display: disable subterm markup removalGravatar David Aspinall2008-08-03
|
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* Revert cursor hide in goals and response to avoid user confusion; use bar ↵Gravatar David Aspinall2008-07-05
| | | | cursor.
* Reduce compiler warnings. Minor fixes.Gravatar David Aspinall2008-01-16
|
* Compilation tweaksGravatar David Aspinall2008-01-16
|
* Revert 8.18: font-lock-append-text-property merges faces better.Gravatar David Aspinall2008-01-16
|
* pg-response-display: use add-text-properties instead of ↵Gravatar David Aspinall2008-01-15
| | | | font-lock-append-text-property [no behaviour change]
* Many rearrangements for compatibility, efficient/correct compilation, ↵Gravatar David Aspinall2008-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 ↵Gravatar David Aspinall2007-12-14
| | | | output.
* Emacs compatibility/API updates: string-to-int -> string-to-numberGravatar David Aspinall2007-12-10
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 12:18:24 +0000