| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-08-20 | eliminated superficial ';'s; | Makarius Wenzel | |
| 1999-08-20 | update by DvO; | Makarius Wenzel | |
| 1999-08-18 | proof-shell-start-goals-regexp: include \n; | Makarius Wenzel | |
| isa-init-syntax-table moved to isa-syntax.el; improved isa-update-thy-only; | |||
| 1999-08-18 | isa-init-syntax-table moved here from isa.el; | Makarius Wenzel | |
| 1999-08-18 | replaced 'ProofGeneral' by 'Proof General'; | Makarius Wenzel | |
| 1999-08-18 | obsolete; | Makarius Wenzel | |
| 1999-08-16 | obsolete, use Isabelle's native ProofGeneral.init instead; | Makarius Wenzel | |
| 1999-08-16 | proof-shell-first-special-char ?\350; | Makarius Wenzel | |
| tuned prompt; deactivated "No subgoals!"; use Isabelle's native ProofGeneral.init; proper setup for theory loader actions: better handling of multiple buffers; isa-find-and-forget does nothing; | |||
| 1999-08-06 | tuned; | Makarius Wenzel | |
| 1999-08-06 | ProofGeneral interface wrapper for Isabelle/classic | Makarius Wenzel | |
| 1999-07-03 | Removed extra parenthesis. | David Aspinall | |
| 1999-07-02 | fixed some regexp via proof-anchor-regexp; | Makarius Wenzel | |
| 1999-05-27 | renamed proof-commands-regexp to proof-indent-commands-regexp, which | Makarius Wenzel | |
| is less confusing); | |||
| 1999-02-03 | fixed syntax entry for "_" | Thomas Kleymann | |
| 1999-02-01 | Regexp bug. Use proof-string-match appropriately. | David Aspinall | |
| 1999-01-12 | Changed read-no-blanks-input to read-string, former is defunct. | David Aspinall | |
| 1998-12-18 | File sent by David von Oheimb. | David Aspinall | |
| 1998-12-15 | Docstring tweak | David Aspinall | |
| 1998-12-15 | Fixed broken check on proof-mode-hook. | David Aspinall | |
| 1998-12-15 | made many minor changes to the documentation | Thomas Kleymann | |
| 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-10 | Fix for splash hack for theory files when proo-splash-inhibit=t. | David Aspinall | |
| 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 | Documentation improvements. | David Aspinall | |
| 1998-11-25 | FSF Emacs fix for buffer-file-truename, which is the | David Aspinall | |
| *abbreviated* form of file-truename! | |||
| 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-25 | Docstring fixes, minor improvements. | David Aspinall | |
| 1998-11-25 | Docstring fixes | 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 | Added isa-update function. Altered settings. | 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 | Added Proof General menu to theory file mode. | David Aspinall | |
| 1998-11-18 | Added clear_response_buffer regexp, use_thy_and_update now in ProofGeneral | David Aspinall | |
| 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-18 | new file to factor out improved theory reader junk. | David Aspinall | |
| 1998-11-12 | Bug in regexp | David Aspinall | |
| 1998-11-12 | In a fit of autocracy, removed proof-tags-support, binding for | David Aspinall | |
| M-tab and appearance of Find Tags in PG menu. The menu entry already appears in Tools->Tags, and users should bind M-tab for themselves. | |||
| 1998-11-12 | Fixed error regexp | David Aspinall | |
| 1998-11-12 | Fixed a regexp. | David Aspinall | |
| 1998-11-12 | Replaced custom-set-variables with customize-set-variable: | David Aspinall | |
| the first one sets the *saved* value for variables, rather than default values. | |||
| 1998-11-10 | Disabled problematic requires temporarily. | David Aspinall | |
| 1998-11-10 | Removed references of proof-shell-noise-regexp | Thomas Kleymann | |
| 1998-11-10 | Fixes for byte compilations and missing bits of Isamode. | David Aspinall | |
| 1998-11-09 | Removed superfluous variable. Improved docstrings. | David Aspinall | |
| 1998-11-06 | Added prefix arg to thy-find-other-file to use same window | David Aspinall | |
| 1998-11-04 | Added key binding to switch between theory and ML files. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |