| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-11-17 | Fix a few bugs/probs shown up by byte-compiling. | David Aspinall | |
| 1999-11-16 | Strip CRs from minibuf messages for FSF's sake to remove ^Js. Attempt to ↵ | David Aspinall | |
| fix 'no-catch for exited tag' buglet. | |||
| 1999-11-16 | Added proof-mouse-goto-point, moved proof-mouse-track-insert to proof-script | David Aspinall | |
| 1999-11-16 | Fix to shell filter for non-wakeup char instances of PG. | David Aspinall | |
| Fix to proof-shell-insert-loopback-cmd for pbp. Don't call pbp-make-top-span if proof-goal-hyp-fn is unset. Remove extra newline in goals output. Removed some dead code. Made code robust against more settings being unset. Added menu to goals buffer. Set key "q" in response and goals buffers to bury-buffer. Quit timeout variable. | |||
| 1999-11-15 | docstring | David Aspinall | |
| 1999-11-15 | proof-grab-lock calls proof-shell-ready-prover with queuemode arg. ↵ | David Aspinall | |
| Docstring and debug msgs | |||
| 1999-11-15 | Fix for FSF Emacs. Added timeout arg to proof-shell-wait. | David Aspinall | |
| 1999-11-14 | Many robustness improvements for error and interrupt handling: | David Aspinall | |
| - Introduce proof-shell-error-or-interrupt-seen flag set after an error or interrupt was seen (in fact, on every call to proof-release-lock). Examine it in proof-activate-scripting to see whether hooks succeeded in activating scripting. - Test in the shell filter for the lock being held yet nothing in the action list, and clear the lock if so. Gets rid of repetetive proof-shell-busy messages when the queue is empty (for errors during development, or nasty uses of C-g) - Add a timeout to proof-shell-wait (not used yet) | |||
| 1999-11-14 | proof-nested-goals-allowed -> proof-completed-proof-behaviour | David Aspinall | |
| Patch for more flexible handling of closing goal...save regions after proof has been completed. | |||
| 1999-11-13 | comments | David Aspinall | |
| 1999-11-12 | Added ACTION to proof-shell-insert so proof-shell-insert-hook can test class ↵ | David Aspinall | |
| of command. (For Plastic) | |||
| 1999-11-12 | Made display table stuff interactive. | David Aspinall | |
| 1999-11-12 | Fixes for response buffer display, x-symbol, output formatting. | David Aspinall | |
| 1999-11-11 | Added option for sending qed output to goals buffer for Isabelle | David Aspinall | |
| 1999-11-11 | small changes to plastic mode | Paul Callaghan | |
| 1999-11-11 | Next round of fixups for font-lock and x-symbol. | David Aspinall | |
| 1999-11-11 | Extensive fixes for x-symbol and font-lock. | David Aspinall | |
| 1999-11-11 | Patches for urgent message processing. | David Aspinall | |
| 1999-11-10 | Moved utility function proof-files-to-buffers to proof.el. Fixed local var | David Aspinall | |
| 1999-11-09 | Generic support for x-symbol tuned up. | David Aspinall | |
| 1999-11-08 | Provisional updates for x-symbol support (incomplete) | David Aspinall | |
| 1999-10-27 | update of x-symbol stuff by DvO; | Makarius Wenzel | |
| 1999-10-25 | Bug fix for proof-re-end-of-cmd (regexp-quote proof-terminal-string) | David Aspinall | |
| 1999-10-21 | docstring | David Aspinall | |
| 1999-10-15 | FIRST ATTEMPT AT CANY QUEUE HANDLING. Extending regions when advancing patch. | David Aspinall | |
| 1999-10-15 | Failed attempt to fix sentinel problem | David Aspinall | |
| 1999-10-15 | comments added. | David Aspinall | |
| 1999-10-15 | Disabled proliferation of proof shell buffers. | David Aspinall | |
| 1999-10-14 | Docstring | David Aspinall | |
| 1999-10-06 | Comments in proof-shell-filter. | David Aspinall | |
| 1999-10-06 | Speed optimizations, part I. | David Aspinall | |
| 1999-10-06 | Made new command proof-cd to cd to the directory of the current | David Aspinall | |
| buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly. | |||
| 1999-10-06 | Fixed coalescing of error messages: all error messages from | David Aspinall | |
| the last command are now show. Added extra docs to clarify behaviour. | |||
| 1999-10-06 | Added proof-tidy-response user option. | David Aspinall | |
| 1999-10-01 | Fix bug for proof-shell-leave-annotations-in-output. | David Aspinall | |
| 1999-09-29 | Unhappily added proof-shell-leave-annotations-in-output hack. | David Aspinall | |
| 1999-09-29 | Extended documentation for proof-shell-restart. | David Aspinall | |
| 1999-09-29 | Re-enabled proof-by-pointing for testing purposes only. Fixed a bug. | David Aspinall | |
| 1999-09-29 | Improved proof-copy-span and renamed to proof-mouse-track-insert. | David Aspinall | |
| Now will insert into any buffer at point, or behave as mouse-track-insert when called over a non-span (or non-vanilla command span). | |||
| 1999-09-29 | Re-enabled and renamed proof-send-span: becomes proof-copy-span bound to ↵ | David Aspinall | |
| C-button1 | |||
| 1999-09-28 | More reorganizing of menus and keybindings with aim of usability in mind. | David Aspinall | |
| 1999-09-28 | Reorganization of menus: made a single menu but flattened Scripting submenu. | David Aspinall | |
| 1999-09-23 | Trivial. | David Aspinall | |
| 1999-09-22 | proof-completed-regexp: match number 1 is response text; | Makarius Wenzel | |
| 1999-09-22 | Whitespace | David Aspinall | |
| 1999-09-21 | Comment fix. | David Aspinall | |
| Fix for FSF Emacs. | |||
| 1999-09-21 | Robustification so that new instances are easier to add | David Aspinall | |
| (allowed a bunch of regexps to be unset, safely). | |||
| 1999-09-21 | proof-shell-grab-lock runs proof-state-change-hook. | David Aspinall | |
| This results in some flickering of the toolbar (buttons disabled while region is pink), but is The Right Thing. Removed "Inferior" from buffer names. | |||
| 1999-09-21 | Callback for proof-shell-done-invisible now runs proof-state-change-hook. | David Aspinall | |
| 1999-09-13 | Fix so that buffer names are shorter (esp for Coq). | David Aspinall | |
| A fixed version of Patrick's earlier patch. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |