aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-shell.el
AgeCommit message (Collapse)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:23:58 +0000