aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-shell.el
AgeCommit message (Expand)Author
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
2011-09-14Fix typoDavid Aspinall
2011-09-14Remove contentious call to set-process-query-on-exit-flag, ref Trac#424David Aspinall
2011-09-11Fix proof-shell-exit optional argument with (interactive) thanks toPierre Courtieu
2011-04-19* small doc fixHendrik Tews
2011-04-15* fix overwriting setq coq-prog-name before loading Proof GeneralHendrik Tews
2011-03-14- change to proof-restart-buffers for unlocking ancestorsHendrik Tews
2011-02-14put coq compilation feature into coq settings menuHendrik Tews
2011-01-31Improve handling of trace buffer and tracing slow mode.David Aspinall
2011-01-26- more info on the elements of proof-action-list; the COMMANDSHendrik Tews
2011-01-25proof-shell-kill-function: use our own busy loop, as proof-shell-waitDavid Aspinall
2011-01-23proof-shell-exit: mention quit command and quit timeout in docDavid Aspinall
2011-01-23Make proof-shell-quit-timeout a prover-specific customize option, default to ...David Aspinall
2011-01-23Kill prover process without asking on Emacs exitDavid Aspinall
2011-01-18- fixed stale load path problem with killing the proof shell inHendrik Tews
2011-01-18Localise compilation fix for dynamic scope of `queueitems\'.David Aspinall
2011-01-18- fixed compilation errorsHendrik Tews
2011-01-18- fix broken external compilationHendrik Tews
2011-01-14- simple backward compatible change to invoke a function toHendrik Tews
2011-01-12Add preliminary support for multiple files for coq.Hendrik Tews
2010-10-10Adjust a comment on proof-shell-modeDavid Aspinall
2010-10-01Add explicit 'invisible flag on the action list for invisible commands.David Aspinall
2010-10-01proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting in...David Aspinall
2010-09-29Support proof-shell-init-cmd being a listDavid Aspinall
2010-09-29Support proof-shell-init-cmd being a listDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 18:00:41 +0000