| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-12-15 | Fixes for FSF Emacs handling of processes, kill buffer hooks, | David Aspinall | |
| and live/dead overlays. | |||
| 1998-12-15 | made many minor changes to the documentation | Thomas Kleymann | |
| 1998-12-14 | 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 | |
| . added further benefit in last section | |||
| 1998-12-14 | rearrange pages automatically | Thomas Kleymann | |
| 1998-12-14 | fixed bug in lego-shell-adjust-line-width (It now monitors the | Thomas Kleymann | |
| proof-goals-buffer) | |||
| 1998-12-14 | Added section for UITP/TP researchers, mentioning further possible | David Aspinall | |
| projects. Added many more mailing list addresses. Not sure what half of them are, need vetting really. | |||
| 1998-12-11 | 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 | |
| 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? | |||
| 1998-12-11 | 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 | |
| in case the prover asks it to be. This can happen when loading theory files in Isabelle. | |||
| 1998-12-11 | 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 | |
| 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). | |||
| 1998-12-11 | Added new test/comments. | David Aspinall | |
| 1998-12-11 | Updates | David Aspinall | |
| 1998-12-11 | Several changes: | David Aspinall | |
| 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). | |||
| 1998-12-11 | 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 | Removed check for proof script buffer from retraction enabler. | David Aspinall | |
| 1998-12-11 | Fixed typo. | David Aspinall | |
| 1998-12-11 | Name of proof-shell-restart was changed. | David Aspinall | |
| 1998-12-11 | Tidied output by putting newlines before imports done message. | David Aspinall | |
| 1998-12-11 | Fixed bug where proof-activate-scripting nuked locked regions. | David Aspinall | |
| 1998-12-11 | Removed proof-send, now use proof-shell-insert instead. | David Aspinall | |
| Removed proof-preprocess-input hook function, Paul Callaghan can now use proof-shell-insert-hook instead for his need. | |||
| 1998-12-11 | Handy | David Aspinall | |
| 1998-12-11 | Removed proof-shell-preprocess-command. Improved docstring for ↵ | David Aspinall | |
| proof-shell-insert-hooks. | |||
| 1998-12-11 | Explained one-prover issue better. | David Aspinall | |
| 1998-12-11 | . Removed "multiple prover problem" from bugs section, since it's now | David Aspinall | |
| handled gracefully. It's a limitation rather than a bug per se. . Added a new subsection to Appendix A, for setting names of binaries. . Moved the table of script extensions and mode names to section 1.1 . Added proof-shell-insert and proof-invisible command to Chap 10. . Updated magic. | |||
| 1998-12-11 | Removed multiple provers problem, it's handled gracefully now and not a bug. | David Aspinall | |
| 1998-12-11 | Added some items after user feedback. Also some *** probs. | David Aspinall | |
| 1998-12-11 | Updated for version 2.0 | David Aspinall | |
| 1998-12-11 | Disabled span-making part of proof-shell-analyse structure for Emacs 20.3 | David Aspinall | |
| 1998-12-11 | Added mention of FSFmacs multibyte character problem (version 20.3) | David Aspinall | |
| 1998-12-10 | Made point stay at top of goals buffer and bottom of response buffer | David Aspinall | |
| 1998-12-10 | Changed name of proof-toolbar-inhibit variable for uniformity. | David Aspinall | |
| 1998-12-10 | New file mentioning some test cases. | David Aspinall | |
| 1998-12-10 | Offer to save script mode buffers which have no files, | David Aspinall | |
| in case Emacs is exited accidently. (Esoteric improvement). | |||
| 1998-12-10 | Patch for case that new script buffer has no filename. | David Aspinall | |
| 1998-12-10 | Fix for splash hack for theory files when proo-splash-inhibit=t. | David Aspinall | |
| 1998-12-10 | Fix for proof-splash-inhibit = t. Bug report from Paul Callaghan. | David Aspinall | |
| 1998-12-08 | o special characters are no longer displayed in (16Bit) FSF GNU Emacs | Thomas Kleymann | |
| 20.3 o however, there is still a mysterious bug in 'proof-shell-analyse-structure' when processing lego/example.l | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |