Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Changed title of Chap 10. | David Aspinall | 1998-12-15 | |
| | ||||
* | Set version tag for new release. | David Aspinall | 1998-12-15 | |
| | ||||
* | Preface: Added David von Oheimb to credits. Mentioned adding multiple files. | David Aspinall | 1998-12-15 | |
| | ||||
* | Updated magic. | David Aspinall | 1998-12-15 | |
| | ||||
* | Used authorized keywords. | David Aspinall | 1998-12-15 | |
| | ||||
* | Docstring fix. | David Aspinall | 1998-12-15 | |
| | ||||
* | Made preface unnumbered. Cosmetic improvements. Updated magic. | David Aspinall | 1998-12-15 | |
| | ||||
* | Docstring fixes | David Aspinall | 1998-12-15 | |
| | ||||
* | Docstring fix | David Aspinall | 1998-12-15 | |
| | ||||
* | credits now at the beginning | Thomas Kleymann | 1998-12-15 | |
| | ||||
* | Another todo idea added. This version sent to Emacs news groups. | David Aspinall | 1998-12-15 | |
| | ||||
* | Idea for magical texi-docstring property for symbols to escape auto markup. | David Aspinall | 1998-12-15 | |
| | ||||
* | Documented markup rules and usage at start of package. | David Aspinall | 1998-12-15 | |
| | ||||
* | Improved documentation of proof-included-files-list. | David Aspinall | 1998-12-15 | |
| | ||||
* | *** empty log message *** | Thomas Kleymann | 1998-12-15 | |
| | ||||
* | Added ps to make all. | David Aspinall | 1998-12-15 | |
| | ||||
* | Fixed several typos. | David Aspinall | 1998-12-15 | |
| | | | | | | Added docstring for proof-deactivate-scripting and mentioned it in Chap 10. Removed spurious mention of defunct function proof-restart-scripting. | |||
* | Updated magic. Small changes in Chap 11. | David Aspinall | 1998-12-15 | |
| | ||||
* | Added back magic target, handy to force update of magic. | David Aspinall | 1998-12-15 | |
| | ||||
* | Removed done stuff. Added LEGO cd hook todo. | David Aspinall | 1998-12-15 | |
| | ||||
* | radical new version of Credits and References section | Thomas Kleymann | 1998-12-15 | |
| | ||||
* | Fixed broken check on proof-mode-hook. | David Aspinall | 1998-12-15 | |
| | ||||
* | Removed bogus duplicate call of proof-mode-hook at end of proof-config-done. | David Aspinall | 1998-12-15 | |
| | ||||
* | Fixes for FSF Emacs handling of processes, kill buffer hooks, | David Aspinall | 1998-12-15 | |
| | | | | and live/dead overlays. | |||
* | made many minor changes to the documentation | Thomas Kleymann | 1998-12-15 | |
| | ||||
* | Altered order of new para and removed some mailing list addrs | David Aspinall | 1998-12-14 | |
| | ||||
* | Another FSF bug found in the new filter functions, this time for script buffer. | David Aspinall | 1998-12-14 | |
| | ||||
* | Gave up on buggy Emacs 19 support, now give error for Emacs 19. | David Aspinall | 1998-12-14 | |
| | ||||
* | Reordered require of cl. Changed deflocal definition. | David Aspinall | 1998-12-14 | |
| | ||||
* | Log of testing results. | David Aspinall | 1998-12-14 | |
| | ||||
* | . modified mailing lists | Thomas Kleymann | 1998-12-14 | |
| | | | | . added further benefit in last section | |||
* | rearrange pages automatically | Thomas Kleymann | 1998-12-14 | |
| | ||||
* | fixed bug in lego-shell-adjust-line-width (It now monitors the | Thomas Kleymann | 1998-12-14 | |
| | | | | proof-goals-buffer) | |||
* | Added section for UITP/TP researchers, mentioning further possible | David Aspinall | 1998-12-14 | |
| | | | | | | | projects. Added many more mailing list addresses. Not sure what half of them are, need vetting really. | |||
* | Set version tag for new release. | David Aspinall | 1998-12-11 | |
| | ||||
* | More comments about multiple file problems | David Aspinall | 1998-12-11 | |
| | ||||
* | Disabled hack for proof-shell-process-file which allowed | David Aspinall | 1998-12-11 | |
| | | | | | | | | | | | empty string to stand for filename of current scripting buffer. This added the current script buffer onto the included files list immediately processing it began (if it began with something creating a mark). However, I removed the check for the current scripting buffer so that that could correctly be marked atomic for Isabelle at other times. This resulted in current buffer being marked atomic, and errors. Are there still more errors? | |||
* | Comments | David Aspinall | 1998-12-11 | |
| | ||||
* | Urgent fix for multiple files wanted. | David Aspinall | 1998-12-11 | |
| | ||||
* | Allow even the current scripting buffer to be marked atomically | David Aspinall | 1998-12-11 | |
| | | | | | in case the prover asks it to be. This can happen when loading theory files in Isabelle. | |||
* | More test cases mentioned | David Aspinall | 1998-12-11 | |
| | ||||
* | todo for Isabelle multiple files. | David Aspinall | 1998-12-11 | |
| | ||||
* | Altered behaviour to allow retraction part-way through finished scripts. | David Aspinall | 1998-12-11 | |
| | | | | | | | | Previously Proof General was asked to unlock a file A.ML as soon as retraction in it happened. Now Proof General is only asked to unlock the children of A.ML, although Isabelle records the fact that A.ML has been retracted. (Which means that if A.ML is later re-linked, Proof General will correctly get told about it). | |||
* | Added new test/comments. | David Aspinall | 1998-12-11 | |
| | ||||
* | Updates | David Aspinall | 1998-12-11 | |
| | ||||
* | Several changes: | David Aspinall | 1998-12-11 | |
| | | | | | | | | | | | | | | | | | | | | | | 1. save-some-buffers now skips the current active scripting buffer. It was annoying to be asked whether to save this one as the user may have just begun typing into a fresh file, or may want to experiment with a modified proof, for example. 2. proof-deactivate-scripting improved so it works pretty well as a (so far undocumented) command. Kill buffer function now removes spans, so that they remain if we deactivate without killing. Plan is to call this in proof-activate-scripting to turn off current scripting buffer and munge the processed file list the way we like it. 3. In both proof-deactivate-scripting and proof-activate-scripting, we do the same thing: files with empty locked regions are removed from the processed files list, those with full locked regions are added. This is an attempt to harmonize the file handling of the theorem prover and whatever it reports with the scripting inside Proof General. Additionally proof-deactivate-scripting retracts a file with a partly locked region, only the active scripting buffer is allowed such a region (currently). | |||
* | Added more commands for testing | David Aspinall | 1998-12-11 | |
| | ||||
* | Added submit bug report to proof-shared-menu | David Aspinall | 1998-12-11 | |
| | ||||
* | Tweaked headings for bug report | David Aspinall | 1998-12-11 | |
| | ||||
* | Added proof-submit-bug-report | David Aspinall | 1998-12-11 | |
| |