| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2010-08-03 | proof-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-01 | proof-splice-separator -> mapconcat builtin | David Aspinall | |
| 2009-11-30 | Replace proof-locked-end -> proof-unprocessed-begin | David Aspinall | |
| 2009-09-16 | Fix compile warnings | David Aspinall | |
| 2009-09-16 | Fix logic handling delayed callbacks and silent stop/start | David Aspinall | |
| 2009-09-15 | Fix doc | David Aspinall | |
| 2009-09-14 | Propertize Scripting modeline indicator. Support error spans. | David Aspinall | |
| 2009-09-10 | Disable process-adaptive-read-buffering: massive slow down for short | David Aspinall | |
| commands (certainly when the value is persisted). | |||
| 2009-09-10 | Experimental changes to queue several commands at once and to allow ↵ | David Aspinall | |
| pre-processing of commands when they're queued from script | |||
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-09 | Prevent font-lock in shell by altering font-lock-global-modes locally | David Aspinall | |
| 2009-09-09 | Clear 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-09 | Simplify output processing; delay some goals/response classification | David 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-08 | proof-shell-handle-error-output: renamed, and simplified | David Aspinall | |
| to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup. | |||
| 2009-09-07 | Whitespace | David Aspinall | |
| 2009-09-06 | Make sure proof-shell-last-output, proof-shell-last-prompt and | David Aspinall | |
| proof-shell-delayed-ouput remain non-nil. | |||
| 2009-09-06 | Reorganisation to avoid generating many intermediate strings from | David 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-05 | Clean whitespace | David Aspinall | |
| 2009-09-04 | replace-in-string -> replace-regexp-in-string | David Aspinall | |
| 2009-09-04 | Define a cleanup function to run intermittently or by hand, avoiding ↵ | David Aspinall | |
| pg-remove-specials. | |||
| 2009-09-04 | Remove proof-shell-prompt-pattern, no longer used. | David Aspinall | |
| 2009-09-04 | Require on scomint in right place | David Aspinall | |
| 2009-09-04 | Possible bug in interrupt signaling discovered | David Aspinall | |
| 2009-09-04 | Use scomint instead of comint | David Aspinall | |
| 2009-09-03 | Shorten startup message | David Aspinall | |
| 2009-08-28 | Fix compile warnings | David Aspinall | |
| 2009-08-20 | Doc tweaks via checkdoc. | David Aspinall | |
| 2009-08-20 | Documentation 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-19 | proof-shell-insert: add scriptspan argument, to pass source positions to ↵ | David Aspinall | |
| proof-shell-insert-hook | |||
| 2009-08-17 | Move proof-interrupt-process to proof-shell. Add pending interrupt ↵ | David Aspinall | |
| behaviour. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179 | |||
| 2009-08-14 | Start refactoring to support more sophisticated queue handling, by adding ↵ | David Aspinall | |
| flags to proof action list | |||
| 2009-08-07 | rename: proof-full-decoration -> proof-full-annotation | David Aspinall | |
| 2009-05-27 | Cleanup more Emacs compatibility | David Aspinall | |
| 2009-05-26 | Add proof state hover messages to proof script, along with useful customization. | David Aspinall | |
| 2009-05-26 | Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor ↵ | David Aspinall | |
| cleanups | |||
| 2009-03-31 | recovered proof-shell-process-urgent-message, by re-introducing ↵ | Makarius Wenzel | |
| commented-out parenthesis and refreshing formerly unreachable cases; | |||
| 2008-08-03 | Disable subterm markup removal | David Aspinall | |
| 2008-07-24 | Merge changes from Version4Branch. | David Aspinall | |
| 2008-07-10 | Minimal patch for Sledgehammer problem with Isabelle. | David Aspinall | |
| Credit due to Makarius. Tested *very briefly* with Coq. See http://proofgeneral.inf.ed.ac.uk/trac/ticket/200 | |||
| 2008-02-06 | Use proof-auxmodes to load auxiliary modes properly when required. | David Aspinall | |
| 2008-01-30 | Fix RCS tags | David Aspinall | |
| 2008-01-30 | Comment cleanups. buffer-substring -> buffer-substring-no-properties. | David Aspinall | |
| 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. | |||
| 2008-01-28 | Add hooks for unicode tokens within proof shell | David Aspinall | |
| 2008-01-25 | split string on proof-rsh-command | David Aspinall | |
| 2008-01-16 | Reduce compiler warnings. Minor fixes. | David Aspinall | |
| 2008-01-16 | Compilation tweaks | David Aspinall | |
| 2008-01-16 | Cleanup compile | David Aspinall | |
| 2008-01-15 | Before calling pg-response-display-with-face, strip eager annotation but not ↵ | David Aspinall | |
| specials. | |||
| 2008-01-15 | Fix cleaning minibuffer echo of urgent messages when proof-shell-unicode is ↵ | David Aspinall | |
| set. Cleanup comments. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |