aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Collapse)Author
2009-09-04Remove configuration of obsolete package function-menu (aka "fume")David Aspinall
2009-09-04Remove configuration of obsolete package function-menu (aka "fume")David Aspinall
2009-09-04Refactoring point movement commands (in progress). Remove proof-no-command.David Aspinall
2009-08-29Cleanup of interactive point moving functions (in progress)David Aspinall
2009-08-28Fix compile warningsDavid Aspinall
2009-08-20Doc tweaks via checkdoc.David Aspinall
2009-08-20proof-one-command-per-line: change default, use in proof-insert-pbp-command.David Aspinall
2009-08-17Only move proof-overlay-arrow once it's got a position.David Aspinall
2009-08-17Move the overlay arrow backwards in case of edits above it whichDavid Aspinall
affect the next position to be processed.
2009-08-14pg-last-output-displayform: add convenience functionDavid Aspinall
2009-08-13Add parser cache for proof-segment-up-to.David Aspinall
2009-08-07proof-colour-locked: complete implementationDavid Aspinall
2009-08-06Prevent setting of proof-overlay-arrow if not configuredDavid Aspinall
2009-07-30Add overlay arrow ported from Kit.David Aspinall
2009-07-30Add proof-colour-locked option to leave locked region background uncoloured.David Aspinall
2009-05-27Check unicode-tokens-mode is boundDavid Aspinall
2009-05-26Add proof state hover messages to proof script, along with useful customization.David Aspinall
2009-05-26proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window: obeyDavid Aspinall
proof-follow-mode=ignore. Ref http://proofgeneral.inf.ed.ac.uk/trac/ticket/187
2009-05-26Revive sendback behaviour (using button1)David Aspinall
2009-05-25Set default value for `buffer-invisibility-spec'David Aspinall
2008-07-24Merge changes from Version4Branch.David Aspinall
2008-07-10Reverse 8.28, buffer-substring-no-properties -> buffer-substring.David Aspinall
This fixes Unicode Tokens handling of sub/super scripts, etc. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/214 Thanks to Simon Winwood for identifying failure point.
2008-01-31Sendback commands from response buffer sent via assert-until-point, with ↵David Aspinall
ordinary span construction.
2008-01-30Documentation.David Aspinall
2008-01-29buffer-substring -> buffer-substring-no-properties since we never use themDavid Aspinall
2008-01-29Comments.David Aspinall
2008-01-29Typo.David Aspinall
2008-01-29proof-set-queue-endpoints: only use undo-discarding function ifDavid Aspinall
undo-make-selective-list is available (not on XEmacs).
2008-01-29Disable undo in read-only region; add proof-allow-undo-in-read-only settingDavid Aspinall
2008-01-25pg-clear-script-portions: fix handling of buffer-invisibility-specDavid Aspinall
(missing apply)
2008-01-24Fixes and cleanups for coq-indent-line, see Trac #172David Aspinall
2008-01-17Disable removal from input historyDavid Aspinall
2008-01-17CommentDavid Aspinall
2008-01-17Add input history ring. Cleanup comments.David Aspinall
2008-01-16Reduce compiler warnings. Minor fixes.David Aspinall
2008-01-16Compilation tweaksDavid Aspinall
2008-01-15Simplify font lock settings, removing proof-font-lock-case-fold-searchDavid Aspinall
2008-01-15Many rearrangements for compatibility, efficient/correct compilation, ↵David Aspinall
namespaces fixes. pre-shell-start-hook: remove this, use default names for modes proof-compat: simplify architecture flags, use standard (featurep 'xemacs).
2007-12-10Modify buffer-invisibility-spec to work smoothly with X-Symbol/EmacsDavid Aspinall
2007-12-09Patch for buggy derived.el in XEmacs 21.5.b28David Aspinall
2007-08-19CommentsDavid Aspinall
2007-08-14Add support for sending back literal commands reusing PBP markup mechanisms.David Aspinall
2007-04-23Clean comments around eval-and-compile proof-modeDavid Aspinall
2007-04-16Fixed a parenthesis, suggested by Stefan Monnier.Pierre Courtieu
2006-04-26Changed the type of proof-goal-command-p. It takes now a span, whichPierre Courtieu
allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
2005-03-21Updated.David Aspinall
2004-10-20fixed a problem with x-symbol not enables in script bufferChristophe Raffalli
2004-10-04Add arg to forward-comment for GNU Emacs.David Aspinall
2004-06-03proof-goto-end-of-locked: add push-mark; fix: goto end of locked even ifDavid Aspinall
buffer switched.
2004-04-26Allow proof-goto-end-of-locked to work again if no active scripting buffer.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 17:11:29 +0000