aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Collapse)Author
2010-10-10pg-span-name: improve docstring.David Aspinall
proof-complete-buffer-atomic: simplify. Add debug message for parser cache.
2010-10-10Fix to last patch.David Aspinall
2010-10-10proof-assert-electric-terminator: prevent adding terminator if point is ↵David Aspinall
after it as well as before, as in PG 3.7. Fixes #371.
2010-10-01Move utility span-make-modifying-removing-span to span.elDavid Aspinall
2010-10-01proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting ↵David Aspinall
input (no non-nil flags in queue)
2010-10-01Adjust handling of insertion of newlines before next command.David Aspinall
2010-09-29DocDavid Aspinall
2010-09-08mapcar -> mapc to fix compile errorDavid Aspinall
2010-09-08Remove debug messageDavid Aspinall
2010-09-08Improve/fix invisibility management, using buffer-invisibility-spec. Adjust ↵David Aspinall
span regions.
2010-09-08Trivial comment changeDavid Aspinall
2010-09-08Tidy comments.David Aspinall
2010-09-07proof-assert-electric-terminator: fix for proof-terminal-string, not charDavid Aspinall
2010-08-27Replace proof-terminal-char with proof-terminal-string.David Aspinall
2010-08-27Implement the eagerly anticipated Beyond Script Management Feature No.2 ↵David Aspinall
(i.e., automatic preview of next command)
2010-08-25Fix compile: declare proof-interrupt-processDavid Aspinall
2010-08-25proof-retract-before-change: now interrupts are robust in Isabelle, tryDavid Aspinall
interrupting if prover is busy before undoing. Refs Trac #293
2010-08-25Bring syntactic context functions togetherDavid Aspinall
2010-08-17Autosend: don't autosend after undoing; add proof-shell-last-queuemode to ↵David Aspinall
support this.
2010-08-17WhitespaceDavid Aspinall
2010-08-17Clean up handling of pending interrupts, remove experimental ↵David Aspinall
proof-shell-interrupts-after-commit.
2010-08-16Fix compile errors, update tagsDavid Aspinall
2010-08-15Preliminary and experimental support for automatically sending commands.David Aspinall
2010-08-13proof-activate-scripting: make sure can succeed whenDavid Aspinall
proof-activate-scripting-hook does nothing (case: switching buffers in Coq when there was an error)
2010-08-11Support custom syntactic fontification. Split out pa macros.David Aspinall
2010-08-08proof-assert-electric-terminator: give more user-friendly error message if ↵David Aspinall
unparseable
2010-08-08Checkdoc cleanupsDavid Aspinall
2010-08-03proof-assert-electric-terminator: fix logic for inserting at buffer endDavid Aspinall
2010-08-03Move key binding for proof assistant keymap (fixes compilation bug)David Aspinall
2010-08-03save-some-buffers: only offer to save proof script buffersDavid Aspinall
2010-08-03Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.David Aspinall
2010-07-08Cleanups for save-excursion to avoid warnings in latest Emacs versionsDavid Aspinall
2009-12-03Rework script span element hiding to avoid buffer-invisibility-spec. Add ↵David Aspinall
command elements.
2009-11-30Fix for Trac #307.David Aspinall
2009-11-30Replace proof-locked-end -> proof-unprocessed-beginDavid Aspinall
2009-11-28Add `proof-script-sticky-error-face' and `proof-sticky-errors' setting.David Aspinall
2009-10-15proof-script-use-old-parser: remove configuration option and cleanupDavid Aspinall
2009-10-14Shorten commentsDavid Aspinall
2009-10-03proof-script-generic-parse-cmdstart: set case-fold-searchDavid Aspinall
proof-inside-string: added
2009-10-03proof-assert-electric-terminator: repair so works at end of bufferDavid Aspinall
2009-10-02proof-retract-before-change: give error if prover busyDavid Aspinall
(see http://proofgeneral.inf.ed.ac.uk/trac/ticket/293)
2009-09-28Functions find-and-forget and count-undos now return lists of commandsDavid Aspinall
2009-09-25pg-toggle-element-visibility: Add back `redraw-frame' call, it *is*David Aspinall
needed here (possible Emacs bug)
2009-09-21Remove redisplay function call for Emacs, seems unnecssary.David Aspinall
2009-09-21Repair some of proof visibility handlingDavid Aspinall
pg-last-output-displayform: protect against single \n in last output
2009-09-20proof-script-clear-queue-spans-on-error: jump to start of error spanDavid Aspinall
(if proof-follow-mode suggests following locked region)
2009-09-20pg-set-span-helphighlights: add hook to delete help highlightDavid Aspinall
on any edit (affects error spans and outdated help spans).
2009-09-20proof-cmdstart-add-segment-for-cmd: classify all whitespace as aDavid Aspinall
comment, not a command.
2009-09-16pg-last-output-displayform: protect against empty stringDavid Aspinall
2009-09-15When calling proof-script-preprocess, fix starting position.David Aspinall
proof-assert-electric-terminator: restore expected behaviour with/without term.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:34:41 +0000