| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | proof-retract-until-point: protect against finding no span at all | David Aspinall | |
| (mask current bug in Coq code) | |||
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-10 | Clean compile | David Aspinall | |
| 2009-09-10 | Move defpacustom here. Move message functions to proof-shell. Fix requires. | David Aspinall | |
| 2009-09-10 | Add proof-minibuffer-messages. Move defpacustom->proof-utils and | David Aspinall | |
| fix requires. | |||
| 2009-09-10 | Add `proof-minibuffer-messages' | David Aspinall | |
| 2009-09-09 | Prevent font-lock in shell by altering font-lock-global-modes locally | David Aspinall | |
| 2009-09-09 | pg-last-output-displayform: strip trailing CR as well as initial one, | David Aspinall | |
| to tidy up popups for Isabelle. | |||
| 2009-09-09 | Delete the pghelp spans for now, after all. | David Aspinall | |
| 2009-09-09 | proof-script-clear-queue-spans: scan less of buffer | David Aspinall | |
| proof-script-delete-spans: leave 'pghelp spans in place for now pg-set-span-helphighlights: add extra FACE argument proof-done-advancing-save, proof-make-goalsave: support proof-arbitrary-undo-positions. | |||
| 2009-09-09 | Add proof-shell-font-lock-keywords, proof-arbitrary-undo-positions | 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 | Add proof-re-search-forward-safe | David Aspinall | |
| 2009-09-09 | p-s-classify-output -> p-s-handle-output, and simplify system-specific hook | David Aspinall | |
| 2009-09-09 | Add proof-script-error-face | David Aspinall | |
| 2009-09-09 | proof-shell-error-or-interrupt-seen -> proof-shell-last-error-kind, | David Aspinall | |
| as per previous proof-shell update. | |||
| 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-09 | proof-shell-quiet-errors: move to user opts custom group | David Aspinall | |
| 2009-09-09 | Cleanup toolbar-toggle and bind to C-c b, fix binding C-c v. | David Aspinall | |
| Add "Beep on Errors" setting to menu | |||
| 2009-09-09 | proof-toolbar-setup: redraw-display | David Aspinall | |
| 2009-09-09 | proof-toolbar-setup: do the right thing (map across all PG buffers) | David Aspinall | |
| 2009-09-08 | proof-kill-goal-command: default to nil, not empty string | David Aspinall | |
| 2009-09-08 | Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵ | David Aspinall | |
| LEGO messages) | |||
| 2009-09-08 | Clarify require | David Aspinall | |
| 2009-09-08 | Require on scomint | David Aspinall | |
| 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-08 | Fix docstrings, remove spurious null | David Aspinall | |
| 2009-09-08 | pg-response-display-with-face: remove update of `proof-shell-last-output' | David Aspinall | |
| 2009-09-07 | Only show splash message if noninteractive | David Aspinall | |
| 2009-09-07 | Remove load order tweak experiment | David Aspinall | |
| 2009-09-07 | Nuke spurious warning | David Aspinall | |
| 2009-09-07 | Update autoloads | David Aspinall | |
| 2009-09-07 | Attempt to handle splash buffer cleanly. | David Aspinall | |
| 2009-09-07 | Requires processed more often (experiment) | David Aspinall | |
| 2009-09-07 | Fix compile warnings | David Aspinall | |
| 2009-09-07 | Whitespace | David Aspinall | |
| 2009-09-07 | (C) date | David Aspinall | |
| 2009-09-07 | mapcar -> dolist | David Aspinall | |
| 2009-09-07 | Require cl for compilation | David Aspinall | |
| 2009-09-07 | Missing require | David Aspinall | |
| 2009-09-07 | Fix typos | David Aspinall | |
| 2009-09-06 | Typo | David Aspinall | |
| 2009-09-06 | Avoid easy-menu-define macro | David Aspinall | |
| 2009-09-06 | Updated | David Aspinall | |
| 2009-09-06 | Make sure proof-shell-last-output is non-nil | David Aspinall | |
| 2009-09-06 | pg-add-element: unbound var in debug | David Aspinall | |
| proof-activate-scripting: minor cleanup proof-assert-until-point: don't go back beyond end of locked | |||
| 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-06 | Include macros for compile | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |