aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Collapse)Author
2011-01-24- change 'span-delete-action in 'span-delete-actions, which isHendrik Tews
now a list of functions to be run when the span is deleted. Use span-add-delete-action to add a delete action.
2011-01-23proof-protected-process-or-retract: don't give failure error if nothing to doDavid Aspinall
Addresses Trac #383
2011-01-19pg-show-all-portions: protect against empty hash tablesDavid Aspinall
2011-01-14- move proof-no-fully-processed-buffer to generic/proof-configHendrik Tews
- add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted
2011-01-12Add preliminary support for multiple files for coq.Hendrik Tews
The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names
2010-10-11proof-segment-up-to-using-cache: improve attemptDavid Aspinall
2010-10-10Fix debug message formatDavid Aspinall
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:37:11 +0000