| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2009-09-06 | Compile with cl. Fix typo. | David Aspinall | |
| 2009-09-06 | proof-clean-buffer: inhibit read only | David Aspinall | |
| 2009-09-06 | Change type of proof-shell-process-file, proof-shell-compute-new-files-list | David Aspinall | |
| 2009-09-06 | Fix compile warnings | David Aspinall | |
| 2009-09-06 | Tweak point movement in `proof-assert-until-point' and | David Aspinall | |
| alter meaning of `proof-only-whitespace-to-locked-region-p'; both now refer to char after point. Script elements are now stored in hash tables rather than lists. | |||
| 2009-09-06 | Rearrange some of point movement code for following scripting. | David Aspinall | |
| 2009-09-06 | pg-xml-parse-buffer: generalise to take region arguments. | David Aspinall | |
| 2009-09-06 | Clarify that eager message matches are now anchored | David Aspinall | |
| 2009-09-06 | Remove use-specials-for-fontify | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |