aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-shell.el
AgeCommit message (Collapse)Author
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
2010-08-03proof-shell-wait, proof-shell-kill-function: avoid use of sit-for.David Aspinall
2010-06-27`proof-shell-process-urgent-messages': fix to avoid duplicated messages ↵David Aspinall
(Trac#314) `proof-shell-exit': fix pareno, avoid duplicated user question in Emacs 23. Consistent capitalisation of errors.
2009-12-01proof-splice-separator -> mapconcat builtinDavid Aspinall
2009-11-30Replace proof-locked-end -> proof-unprocessed-beginDavid Aspinall
2009-09-16Fix compile warningsDavid Aspinall
2009-09-16Fix logic handling delayed callbacks and silent stop/startDavid Aspinall
2009-09-15Fix docDavid Aspinall
2009-09-14Propertize Scripting modeline indicator. Support error spans.David Aspinall
2009-09-10Disable process-adaptive-read-buffering: massive slow down for shortDavid Aspinall
commands (certainly when the value is persisted).
2009-09-10Experimental changes to queue several commands at once and to allow ↵David Aspinall
pre-processing of commands when they're queued from script
2009-09-10Clean compileDavid Aspinall
2009-09-09Prevent font-lock in shell by altering font-lock-global-modes locallyDavid Aspinall
2009-09-09Clear shell buffer contents on restart.David Aspinall
proof-shell-classify-output-system-specific -> proof-shell-handle... and simplify system specific hook. Repair error handling for Isabelle (search forward for matches) Add proof-shell-font-lock-keywords.
2009-09-09Simplify output processing; delay some goals/response classificationDavid Aspinall
until postponed goals/response output drawn. Remove some internal variables. Slightly generalise message model to include Coq 8.1's MESSAGE GOALS output form. Improve documentation of proof-shell-filter and friends to explain this.
2009-09-08proof-shell-handle-error-output: renamed, and simplifiedDavid Aspinall
to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup.
2009-09-07WhitespaceDavid Aspinall
2009-09-06Make sure proof-shell-last-output, proof-shell-last-prompt andDavid Aspinall
proof-shell-delayed-ouput remain non-nil.
2009-09-06Reorganisation to avoid generating many intermediate strings fromDavid Aspinall
the shell buffer, and match shell regexp directly inside it. This changes the types of several configuration settings. Also some improvements to scomint configuration and changes to proof-shell-exec-loop to send the next command to the prover before starting to process the output from the last. This reorganisation is still in testing and will take time to bed down.
2009-09-05Clean whitespaceDavid Aspinall
2009-09-04replace-in-string -> replace-regexp-in-stringDavid Aspinall
2009-09-04Define a cleanup function to run intermittently or by hand, avoiding ↵David Aspinall
pg-remove-specials.
2009-09-04Remove proof-shell-prompt-pattern, no longer used.David Aspinall
2009-09-04Require on scomint in right placeDavid Aspinall
2009-09-04Possible bug in interrupt signaling discoveredDavid Aspinall
2009-09-04Use scomint instead of comintDavid Aspinall
2009-09-03Shorten startup messageDavid Aspinall
2009-08-28Fix compile warningsDavid Aspinall
2009-08-20Doc tweaks via checkdoc.David Aspinall
2009-08-20Documentation improvements.David Aspinall
Experiment with `process-adaptive-read-buffering' Do not run `proof-shell-insert-hook' if input string is empty or single CR.
2009-08-19proof-shell-insert: add scriptspan argument, to pass source positions to ↵David Aspinall
proof-shell-insert-hook
2009-08-17Move proof-interrupt-process to proof-shell. Add pending interrupt ↵David Aspinall
behaviour. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179
2009-08-14Start refactoring to support more sophisticated queue handling, by adding ↵David Aspinall
flags to proof action list
2009-08-07rename: proof-full-decoration -> proof-full-annotationDavid Aspinall
2009-05-27Cleanup more Emacs compatibilityDavid Aspinall
2009-05-26Add proof state hover messages to proof script, along with useful customization.David Aspinall
2009-05-26Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor ↵David Aspinall
cleanups
2009-03-31recovered proof-shell-process-urgent-message, by re-introducing ↵Makarius Wenzel
commented-out parenthesis and refreshing formerly unreachable cases;
2008-08-03Disable subterm markup removalDavid Aspinall
2008-07-24Merge changes from Version4Branch.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 05:06:08 +0000