| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2009-09-15 | Fix compile warning | David Aspinall | |
| 2009-09-15 | Prevent compile warnings | David Aspinall | |
| 2009-09-14 | Adjust comment | David Aspinall | |
| 2009-09-14 | Moved function | David Aspinall | |
| 2009-09-14 | Fix compile issues | David Aspinall | |
| 2009-09-14 | proof-span-give-warning: no message if inhibit-read-only is set | David Aspinall | |
| 2009-09-14 | proof-imenu-enable: fix remove call | David Aspinall | |
| 2009-09-14 | proof-strict-read-only: Experimental change to default | David Aspinall | |
| 2009-09-14 | Doc | David Aspinall | |
| 2009-09-14 | Propertize Scripting modeline indicator. Support error spans. | David Aspinall | |
| 2009-09-14 | Move insert-electric-terminator here. Add experimental error spans. Doc ↵ | David Aspinall | |
| improvements | |||
| 2009-09-14 | Engage which-function mode with imenu. Move insert-electric-terminator to ↵ | David Aspinall | |
| proof-script | |||
| 2009-09-14 | Reorganisation Options with Minor Mode submenu | David Aspinall | |
| 2009-09-11 | Fix docs | David Aspinall | |
| 2009-09-11 | Make quiet by default. Improve docs. | David Aspinall | |
| 2009-09-11 | Our own buffer for debug messages | David Aspinall | |
| 2009-09-11 | Add Read-Only sub menu | David Aspinall | |
| 2009-09-10 | Default to disabling minibuffer messages | David Aspinall | |
| 2009-09-10 | Disable debug message in Isar | 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 | Move stripping and minibuffer-message function here | David Aspinall | |
| 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 | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |