Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Support linear_undo. Add minimal font-lock for readability in *isabelle*. | 2009-09-09 | |
| | |||
* | proof-script-clear-queue-spans: scan less of buffer | 2009-09-09 | |
| | | | | | | 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. | ||
* | Add proof-shell-font-lock-keywords, proof-arbitrary-undo-positions | 2009-09-09 | |
| | |||
* | Clear shell buffer contents on restart. | 2009-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. | ||
* | Add proof-re-search-forward-safe | 2009-09-09 | |
| | |||
* | p-s-classify-output -> p-s-handle-output, and simplify system-specific hook | 2009-09-09 | |
| | |||
* | Add proof-script-error-face | 2009-09-09 | |
| | |||
* | Add compatilibity for declare-function in Emacs 22.1 | 2009-09-09 | |
| | |||
* | proof-shell-error-or-interrupt-seen -> proof-shell-last-error-kind, | 2009-09-09 | |
| | | | | as per previous proof-shell update. | ||
* | Simplify output processing; delay some goals/response classification | 2009-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-quiet-errors: move to user opts custom group | 2009-09-09 | |
| | |||
* | Cleanup toolbar-toggle and bind to C-c b, fix binding C-c v. | 2009-09-09 | |
| | | | | Add "Beep on Errors" setting to menu | ||
* | proof-toolbar-setup: redraw-display | 2009-09-09 | |
| | |||
* | Another V-8-1 test | 2009-09-09 | |
| | |||
* | proof-toolbar-setup: do the right thing (map across all PG buffers) | 2009-09-09 | |
| | |||
* | Remove more V8 compatibility (thanks to Pierre for carefully highlighting it) | 2009-09-09 | |
| | |||
* | Remove Coq 8.0 code | 2009-09-08 | |
| | |||
* | Remove some spaces | 2009-09-08 | |
| | |||
* | Remove more of 80 code | 2009-09-08 | |
| | |||
* | Updated. | 2009-09-08 | |
| | |||
* | proof-kill-goal-command: default to nil, not empty string | 2009-09-08 | |
| | |||
* | Simplify coq-find-and-forget and drop v80 version | 2009-09-08 | |
| | |||
* | Remove system-specific code as message before goals handled in core now. ↵ | 2009-09-08 | |
| | | | | Alter proof-shell-start-goals-regexp to work in buffer. | ||
* | Comments | 2009-09-08 | |
| | |||
* | Update, remove proof-shell-abort-goal-regexp | 2009-09-08 | |
| | |||
* | Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize ↵ | 2009-09-08 | |
| | | | | LEGO messages) | ||
* | More text about Unicode Tokens | 2009-09-08 | |
| | | | | Remove proof-shell-abort-goal-regexp | ||
* | Comments | 2009-09-08 | |
| | |||
* | Oops: repair hybrid output broken by two window fix! See trac #109. | 2009-09-08 | |
| | |||
* | byte-compile-and-load on write is a bit too enthusiastic | 2009-09-08 | |
| | |||
* | Repair two-window working mode for when Coq doesn't produce hybrid output. | 2009-09-08 | |
| | | | | | | Print Proof -> just Print in context menu. Temporarily inhibit read only in response buffer for error highlighting. Reduce time for error highlighting | ||
* | Clarify require | 2009-09-08 | |
| | |||
* | Require on scomint | 2009-09-08 | |
| | |||
* | proof-shell-handle-error-output: renamed, and simplified | 2009-09-08 | |
| | | | | | to use suggestion to take message from `proof-shell-last-output', now that is no longer munged to remove markup. | ||
* | Fix docstrings, remove spurious null | 2009-09-08 | |
| | |||
* | pg-response-display-with-face: remove update of `proof-shell-last-output' | 2009-09-08 | |
| | |||
* | Remove use of regexp-opt-depth and clarify doc of | 2009-09-08 | |
| | | | | | `unicode-tokens-token-match-regexp'. Fix typo in `proof-tactical-name-face'. | ||
* | Remove devel. from testall target | 2009-09-08 | |
| | |||
* | Remove warnings in batch compile about functions possibly undefined at | 2009-09-08 | |
| | | | | | runtime. Most of these are spurious (come from autoloads; byte comp seems to give these higher priority than declarations in same file). | ||
* | Only show splash message if noninteractive | 2009-09-07 | |
| | |||
* | Remove load order tweak experiment | 2009-09-07 | |
| | |||
* | Nuke spurious warning | 2009-09-07 | |
| | |||
* | Update autoloads | 2009-09-07 | |
| | |||
* | Fix proof-shell-trace-output-regexp: match on annotation \^AI now too | 2009-09-07 | |
| | |||
* | Deleted file | 2009-09-07 | |
| | |||
* | Require unicode-tokens during compile. | 2009-09-07 | |
| | |||
* | scomint-check-proc: make defsubst | 2009-09-07 | |
| | |||
* | Attempt to handle splash buffer cleanly. | 2009-09-07 | |
| | |||
* | Revert change in 10.26 to use defpacustom after all, this gives | 2009-09-07 | |
| | | | | | the prover-specific menu entry automatically. Fix compiler warning with a defvar. | ||
* | Fix initialisation of isar-use-find-theorems-form in compiled file. | 2009-09-07 | |
| |