| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-08-16 | obsolete, use Isabelle's native ProofGeneral.init instead; | Makarius Wenzel | |
| 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-11-26 | Added clear-goals-buffer stuff, asked for response to be left after use_thy. | David Aspinall | |
| 1998-11-25 | Cleaned up, and made use_thy remove ML file from DB properly; | David Aspinall | |
| optimised use_thy to report only on files newly added to db. | |||
| 1998-11-25 | Fixed show_context | David Aspinall | |
| 1998-11-25 | Fixes to debug long standing not-showing-first-goal problem. | David Aspinall | |
| 1998-11-25 | Added Isamode-like keybinding C-c C-l for proof-prf. | David Aspinall | |
| 1998-11-20 | Improvements for multiple files and robustness: keep a copy of | David Aspinall | |
| the initial theory database state, and add a restart command. | |||
| 1998-11-18 | Improvements for multiple files. Now saves state specially for ProofGeneral. | David Aspinall | |
| 1998-11-18 | Fixed problem with list_loaded_files and update(). | David Aspinall | |
| Now when doing use_thy, we don't do an update. Hopefully "following children are out of date" message will be superfluous because they will be unlocked already. Will be re-read as needed. Added update function. Fixed up implementation of list_parents. | |||
| 1998-11-18 | Improvements and cleanups: | David Aspinall | |
| . Put functions into ProofGeneral structure . Annotations around ordinary output appear before cr's . Added clear_response_buffer functionw . Added special_theories to avoid looking up filenames of theories which don't have them | |||
| 1998-11-12 | Fixed error regexp | David Aspinall | |
| 1998-11-03 | Disabled annotated prompts because of strange bug. | David Aspinall | |
| 1998-11-02 | Changes suggested by Markus Wenzel | David Aspinall | |
| 1998-10-29 | Fixes for multiple files. More defcustoms. | David Aspinall | |
| 1998-10-29 | Begun work on adding more special annotations for Isabelle. | David Aspinall | |
| 1998-10-28 | Improved behaviour of Isabelle multiple files: don't retract parent theory. | David Aspinall | |
| 1998-10-28 | Some experimental code added | David Aspinall | |
| 1998-10-28 | Fixed bug in Isabelle count undos. Now uses undo instead of choplev. | David Aspinall | |
| 1998-10-27 | Work on Isabelle theory reader. | David Aspinall | |
| 1998-10-26 | Changes for locked regions in theory files | David Aspinall | |
| 1998-10-23 | Greatly simplified by new functions in Isabelle | David Aspinall | |
| 1998-10-22 | retract_file also works on files without .thy partners. | David Aspinall | |
| 1998-10-22 | Added notes on Isa multi files, web page improvements | David Aspinall | |
| 1998-10-21 | Improved multiple file implementation | David Aspinall | |
| 1998-10-21 | Used new get_thy_filenames function from Isabelle 98-1 | David Aspinall | |
| 1998-10-19 | Customization for multiple files | David Aspinall | |
| 1998-10-12 | Important regular expression fixes: | David Aspinall | |
| -error-regexp doesn't match warnings now. -annotated-prompt-regexp doesn't match warnings now, and is different from -prompt-regexp. | |||
| 1998-10-02 | changed maintainer information to lego@dcs and isabelle@dcs . | Thomas Kleymann | |
| 1998-10-01 | Updated maintainer tags to remove lego email address. | David Aspinall | |
| 1998-10-01 | Renamed file | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |