aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-shell.el
AgeCommit message (Collapse)Author
2011-10-13To fix pgshell mode, restore proof-shell-insert support for a single string ↵David Aspinall
argument and allow nil setting for proof-shell-start-goals-regexp.
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
Erik Martin-Dorel.
2011-04-19* small doc fixHendrik Tews
2011-04-15* fix overwriting setq coq-prog-name before loading Proof GeneralHendrik Tews
* more complete callback listing in proof-action list doc
2011-03-14- change to proof-restart-buffers for unlocking ancestorsHendrik Tews
- improve internal docs for unlocking
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
list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert.
2011-01-25proof-shell-kill-function: use our own busy loop, as proof-shell-waitDavid Aspinall
expects normal prover IO. Addresses http://proofgeneral.inf.ed.ac.uk/trac/ticket/384
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
45 for Isar. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/384.
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
the deactivation-hook
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
- fix quitting during compilation - substitute "compile" for "recompile" - added documentation
2011-01-14- simple backward compatible change to invoke a function toHendrik Tews
compute the command line arguments for a proof assistant
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-10Adjust a comment on proof-shell-modeDavid Aspinall
2010-10-01Add explicit 'invisible flag on the action list for invisible commands.David Aspinall
This means that certain display actions will always be avoided for non-scripting commands (i.e., hints, anything in `proof-shell-error-or-interrupt-hook').
2010-10-01proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting ↵David Aspinall
input (no non-nil flags in queue)
2010-09-29Support proof-shell-init-cmd being a listDavid Aspinall
2010-09-29Support proof-shell-init-cmd being a listDavid Aspinall
2010-09-21Introduce more colourings for active scripting indicator.David Aspinall
2010-09-08Script mouse face highlighting: new faces/colours for commands and regions, ↵David Aspinall
reinstate comment highlighting.
2010-08-27Replace proof-terminal-char with proof-terminal-string.David Aspinall
2010-08-26Move erase-buffer from associate buffer mode functions, allowing ↵David Aspinall
clone-buffer to work, at least superficially.
2010-08-26proof-shell-display-output-as-response: fix to check for no-response-display,David Aspinall
so that proof-shell-invisible-command-invisible-result does what it says on the tin.
2010-08-26proof-interrupt-process: make sure works from non-proof shell buffers.David Aspinall
2010-08-25proof-shell-handle-error-or-interrupt: prevent an error inDavid Aspinall
an obscure case, attempting to handle delayed output when there is none.
2010-08-24Tidy shell start and quit functionsDavid Aspinall
2010-08-24proof-shell-config-done: send proof-assistant-settings-cmdsDavid Aspinall
individually rather than en-massse, avoiding input buffer size problems (bug?) on Emacs 24 with lengthy Isabelle PGIP commands.
2010-08-20Remove dead codeDavid Aspinall
2010-08-19CommentsDavid Aspinall
2010-08-18Remove redisplay from wait loop, only redisplay on exit. Big speed-upDavid Aspinall
but doesn't reflect changes as they happen.
2010-08-18proof-shell-start: tidy upDavid Aspinall
2010-08-18Correct comment; try setting process-adaptive-read-buffering to nil.David Aspinall
2010-08-17Re Trac #324:David Aspinall
proof-shell-wait: drastically reduce timeout, as some implementations perhaps wait for full time even if process output is received. Set process-adaptive-read-buffering to nil regardless of platform
2010-08-17Autosend: don't autosend after undoing; add proof-shell-last-queuemode to ↵David Aspinall
support this.
2010-08-17proof-shell-action-list-item: fix type for flags as an element, not a cdrDavid Aspinall
2010-08-17Critical sync fix: in pending interrupts case be sure toDavid Aspinall
invoke callbacks before detaching queue. Fix to passing of display flags.
2010-08-17CommentsDavid Aspinall
2010-08-17Clean up handling of pending interrupts, remove experimental ↵David Aspinall
proof-shell-interrupts-after-commit.
2010-08-17Make the modeline indicator change colour. Old XEmacs behaviour restored. ↵David Aspinall
Questionable UI benefit.
2010-08-16Fix compile errors, update tagsDavid Aspinall
2010-08-15proof-shell-interrupts-after-commit: support commit-before-interrupt mode ↵David Aspinall
[experimental/temporary].
2010-08-08Checkdoc cleanupsDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:40:16 +0000