aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-shell.el
AgeCommit message (Expand)Author
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
2020-05-29fix: backtrack for "Show Proof" disabledAnaclet
2020-05-29fix: backtrack wrong type argumentAnaclet
2020-05-29Apply reviews of @erikmdCyril Anaclet
2020-05-29WIP for #487Cyril Anaclet
2020-05-29All case for Show and regex variableCyril Anaclet
2018-12-25Reduce the impact of proof-site, in case PG is not usedStefan Monnier
2018-12-14Fixes the fix of #407. Is this temporary.Pierre Courtieu
2018-12-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
2018-12-12Cleanup patch; Moving defvar to toplevelStefan Monnier
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-06-06Fixing bug #187 by removing trailing spaces from prog name.Pierre Courtieu
2017-05-05Change (eval-when (compile) ...) to (eval-when-compile ...)Clément Pit--Claudel
2017-05-05Merge pull request #157 from ProofGeneral/elpaClément Pit-Claudel
2017-03-13Fixing #167.Pierre Courtieu
2017-03-08Remove unnecessary calls to 'eval-and-compile'Clément Pit--Claudel
2017-02-24Removing spurious debug messages.Pierre Courtieu
2017-02-23Fixing #154.Pierre Courtieu
2017-01-18split emergency-cleanup to handle interrupts properly (fixes #143)Hendrik Tews
2016-12-14fix generic interrupt procedure to interrupt parallel background compilationHendrik Tews
2016-12-14Merge pull request #129 from hendriktews/keep-goinghendriktews
2016-12-14Merge pull request #132 from Matafou/masterPierre Courtieu
2016-12-12remove default absolute name from coq-prog-name, but keep dipsplaying it when...Pierre Courtieu
2016-12-08option coq-compile-keep-going for parallel compilationHendrik Tews
2016-11-30fix 2 compilation warnings (fixes #33)Hendrik Tews
2016-06-10Reset proof-script-buffer to nil if -ready-prover failsClément Pit--Claudel
2015-12-31Fix spurious scrolling of *goals* and *response* buffersClément Pit--Claudel
2015-10-09Trying to not delete frames too eagerly when laying out.Pierre Courtieu
2015-03-09Fixes #503.Pierre Courtieu
2015-02-04cleaned previous commits (generic variable to disable error coloring).Pierre Courtieu
2014-06-04* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.Stefan Monnier
2013-01-15- support bullets and braces in ProoftreeHendrik Tews
2013-01-10fix parallel overlapping calls of proof-shell-filterHendrik Tews
2013-01-03- fix asserting when parallel background compilation is in progressHendrik Tews
2012-11-13- first version of parallel asynchronous compilation for coq inHendrik Tews
2012-11-09Doc for pg-finish-tracing-displayDavid Aspinall
2012-08-16Add option proof-layout-windows-on-visit-file, addressing Trac #444David Aspinall
2012-05-24kill windows showing response and goals buffers on proof-shell-exitHendrik Tews
2012-02-08proof-shell-start: initialise associated buffers before shell mode, so in rig...David Aspinall
2012-01-19TypoDavid Aspinall
2012-01-10Tweak message and display model, in particular, make sure that when aDavid Aspinall
2012-01-09Improve configuration for HOL Light. Allow goals display to be prefixed by i...David Aspinall
2012-01-03merge ProofTreeBranch into main trunk:Hendrik Tews
2011-12-07- protect proof-shell-handle-delayed-output against the case whereHendrik Tews
2011-12-06use the start of proof-shell-end-goals-regexp, as documentedHendrik Tews
2011-11-15Quick stab at support for switching to proof shell when interactive support e...David Aspinall
2011-10-17Add fix and regression test for Trac #138David Aspinall
2011-10-13To fix pgshell mode, restore proof-shell-insert support for a single string a...David Aspinall
2011-09-14fix #421 with solution 1Hendrik Tews