aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Expand)Author
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
2019-06-18Remove pghelp spans when retracting.Pierre Courtieu
2019-04-18Derive proof-mode from prog-modeBenjamin Barenblat
2018-12-26Make coq-mode work without generic/proof-*Stefan Monnier
2018-12-25Reduce the impact of proof-site, in case PG is not usedStefan Monnier
2018-12-22* coq-mode.el: New file to make coq-mode independent from PGStefan Monnier
2018-12-14Fix remaining uses of CL; Make files more declarativeStefan Monnier
2018-12-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
2018-12-12Cleanup patch; Moving defvar to toplevelStefan Monnier
2018-08-25Merge pull request #169 from ProofGeneral/help-span-extendedErik Martin-Dorel
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2017-08-15Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.Erik Martin-Dorel
2017-03-09extend helpspan, issue #158Paul Steckler
2017-03-03Remove default key-binding for proof-electric-terminator-toggle.Erik Martin-Dorel
2016-09-25proof-retract-before-change: Fix #41 by saving/restoring the match data.Erik Martin-Dorel
2016-06-10Reset proof-script-buffer to nil if -ready-prover failsClément Pit--Claudel
2016-01-06Fixing #25.Pierre Courtieu
2015-10-13proof-retract-command-hook added + more auto adjust width in coq mode.Pierre Courtieu
2015-10-12proof-assert-command-hook added + Auto adjust width in coq mode.Pierre Courtieu
2014-06-06Don't mess with overlay priorities.Stefan Monnier
2012-08-16Add option proof-layout-windows-on-visit-file, addressing Trac #444David Aspinall
2012-08-14fix 443 by enforcing that the prover is not busy in proof-retract-until-pointHendrik Tews
2012-06-29* generic/pg-user.el (which-func-modes): Fix compiler declaration.Stefan Monnier
2012-06-09Made a small change in generic code about the setting ofPierre Courtieu
2011-10-13Patch from Tom Prince to fix Emacs 24 byte compilation (replace interactive-p...David Aspinall
2011-06-09Add autoload.David Aspinall
2011-06-08- fix for #408: Only use the buffer name inHendrik Tews
2011-05-30Trac#403: wait for retraction to complete before returning, toDavid Aspinall
2011-05-27ensure (integerp proof-segment-up-to-cache-end), fixes Trac #404David Aspinall
2011-05-26proof-retract-before-change: fix Trac #403 (at least partially) byDavid Aspinall
2011-05-16Patch for Trac#400.David Aspinall
2011-05-12Tweak for `proof-segment-up-to-using-cache': better handling ofDavid Aspinall
2011-05-12Attempted fix for `proof-segment-up-to-using-cache', reDavid Aspinall
2011-05-05- flushed proof-done-advancing-require-function andHendrik Tews
2011-04-26Fix for Trac #397. Needs some exercise.David Aspinall
2011-04-13Add proof-output-tooltips option to turn off output highlighting for people w...David Aspinall
2011-03-14- change to proof-restart-buffers for unlocking ancestorsHendrik Tews
2011-01-31Support mouse action on modeline indicator for scripting modeDavid Aspinall
2011-01-25proof-deactivate-scripting: cleanup this function to make moreDavid Aspinall
2011-01-24- change 'span-delete-action in 'span-delete-actions, which isHendrik Tews
2011-01-23proof-protected-process-or-retract: don't give failure error if nothing to doDavid Aspinall
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
2011-01-12Add preliminary support for multiple files for coq.Hendrik Tews
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
2010-10-10Fix to last patch.David Aspinall
2010-10-10proof-assert-electric-terminator: prevent adding terminator if point is after...David Aspinall