aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
Commit message (Collapse)AuthorAge
* Fix compile warningsGravatar David Aspinall2009-09-16
|
* Fix logic handling delayed callbacks and silent stop/startGravatar David Aspinall2009-09-16
|
* Fix docGravatar David Aspinall2009-09-15
|
* Propertize Scripting modeline indicator. Support error spans.Gravatar David Aspinall2009-09-14
|
* Disable process-adaptive-read-buffering: massive slow down for shortGravatar David Aspinall2009-09-10
| | | | commands (certainly when the value is persisted).
* Experimental changes to queue several commands at once and to allow ↵Gravatar David Aspinall2009-09-10
| | | | pre-processing of commands when they're queued from script
* Clean compileGravatar David Aspinall2009-09-10
|
* Prevent font-lock in shell by altering font-lock-global-modes locallyGravatar David Aspinall2009-09-09
|
* Clear shell buffer contents on restart.Gravatar David Aspinall2009-09-09
| | | | | | | 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.
* Simplify output processing; delay some goals/response classificationGravatar David Aspinall2009-09-09
| | | | | | | 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.
* proof-shell-handle-error-output: renamed, and simplifiedGravatar David Aspinall2009-09-08
| | | | | to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup.
* WhitespaceGravatar David Aspinall2009-09-07
|
* Make sure proof-shell-last-output, proof-shell-last-prompt andGravatar David Aspinall2009-09-06
| | | | proof-shell-delayed-ouput remain non-nil.
* Reorganisation to avoid generating many intermediate strings fromGravatar David Aspinall2009-09-06
| | | | | | | | | | | 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.
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* replace-in-string -> replace-regexp-in-stringGravatar David Aspinall2009-09-04
|
* Define a cleanup function to run intermittently or by hand, avoiding ↵Gravatar David Aspinall2009-09-04
| | | | pg-remove-specials.
* Remove proof-shell-prompt-pattern, no longer used.Gravatar David Aspinall2009-09-04
|
* Require on scomint in right placeGravatar David Aspinall2009-09-04
|
* Possible bug in interrupt signaling discoveredGravatar David Aspinall2009-09-04
|
* Use scomint instead of comintGravatar David Aspinall2009-09-04
|
* Shorten startup messageGravatar David Aspinall2009-09-03
|
* Fix compile warningsGravatar David Aspinall2009-08-28
|
* Doc tweaks via checkdoc.Gravatar David Aspinall2009-08-20
|
* Documentation improvements.Gravatar David Aspinall2009-08-20
| | | | | | Experiment with `process-adaptive-read-buffering' Do not run `proof-shell-insert-hook' if input string is empty or single CR.
* proof-shell-insert: add scriptspan argument, to pass source positions to ↵Gravatar David Aspinall2009-08-19
| | | | proof-shell-insert-hook
* Move proof-interrupt-process to proof-shell. Add pending interrupt ↵Gravatar David Aspinall2009-08-17
| | | | behaviour. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179
* Start refactoring to support more sophisticated queue handling, by adding ↵Gravatar David Aspinall2009-08-14
| | | | flags to proof action list
* rename: proof-full-decoration -> proof-full-annotationGravatar David Aspinall2009-08-07
|
* Cleanup more Emacs compatibilityGravatar David Aspinall2009-05-27
|
* Add proof state hover messages to proof script, along with useful customization.Gravatar David Aspinall2009-05-26
|
* Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor ↵Gravatar David Aspinall2009-05-26
| | | | cleanups
* recovered proof-shell-process-urgent-message, by re-introducing ↵Gravatar Makarius Wenzel2009-03-31
| | | | commented-out parenthesis and refreshing formerly unreachable cases;
* Disable subterm markup removalGravatar David Aspinall2008-08-03
|
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* Minimal patch for Sledgehammer problem with Isabelle.Gravatar David Aspinall2008-07-10
| | | | | Credit due to Makarius. Tested *very briefly* with Coq. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/200
* Use proof-auxmodes to load auxiliary modes properly when required.Gravatar David Aspinall2008-02-06
|
* Fix RCS tagsGravatar David Aspinall2008-01-30
|
* Comment cleanups. buffer-substring -> buffer-substring-no-properties.Gravatar David Aspinall2008-01-30
| | | | | | | | Make proof-shell-handle-output robust against START-REGEXP match fail (can happen if shell buffer is garbled/user-edited). Make proof-shell-insert robust against null STRING (should not happen; development artefact while getting rid of proof-no-command). Update date.
* Add hooks for unicode tokens within proof shellGravatar David Aspinall2008-01-28
|
* split string on proof-rsh-commandGravatar David Aspinall2008-01-25
|
* Reduce compiler warnings. Minor fixes.Gravatar David Aspinall2008-01-16
|
* Compilation tweaksGravatar David Aspinall2008-01-16
|
* Cleanup compileGravatar David Aspinall2008-01-16
|
* Before calling pg-response-display-with-face, strip eager annotation but not ↵Gravatar David Aspinall2008-01-15
| | | | specials.
* Fix cleaning minibuffer echo of urgent messages when proof-shell-unicode is ↵Gravatar David Aspinall2008-01-15
| | | | set. Cleanup comments.
* Many rearrangements for compatibility, efficient/correct compilation, ↵Gravatar David Aspinall2008-01-15
| | | | | | | namespaces fixes. pre-shell-start-hook: remove this, use default names for modes proof-compat: simplify architecture flags, use standard (featurep 'xemacs).
* Cleanup coding system setting, commentsGravatar David Aspinall2007-12-14
|
* Add proof-shell-set-text-representation to disable multibyte characters in ↵Gravatar David Aspinall2007-12-14
| | | | legacy case. Use proof-shell-unicode to control whether bytes 128-255 are stripped from output.
* Munging with input/output encoding; try to make consistent.Gravatar David Aspinall2007-12-14
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 15:40:16 +0000