Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add universal keys to theory mode | 1999-11-29 | |
| | |||
* | Fix to proof-shell-proof-completed-regexp by reverting to previous version. | 1999-11-26 | |
| | |||
* | Patch to proof-shell-proof-completed-regexp to prevent overflow, sent by Markus | 1999-11-23 | |
| | |||
* | Failed attempt to trap C-g during try-update-thy. Left as comments. | 1999-11-18 | |
| | |||
* | Remove some obsolete/unecessary stuff. | 1999-11-17 | |
| | |||
* | Cleanups and a bit more highlighting | 1999-11-16 | |
| | |||
* | Matching goals regexp. Comments. | 1999-11-16 | |
| | |||
* | Removed font-lock settings. Set proof-font-lock-zap-commas=t | 1999-11-15 | |
| | |||
* | Many robustness improvements for error and interrupt handling: | 1999-11-14 | |
| | | | | | | | | | | | | - 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) | ||
* | proof-nested-goals-allowed -> proof-completed-proof-behaviour | 1999-11-14 | |
| | | | | | Patch for more flexible handling of closing goal...save regions after proof has been completed. | ||
* | Fixes for Isabelle in case theory file is visited before script file. | 1999-11-12 | |
| | |||
* | Display qed message in goals buffer | 1999-11-12 | |
| | |||
* | Extensive fixes for x-symbol and font-lock. | 1999-11-11 | |
| | |||
* | Fixes for x-symbol activation/deactivation strings | 1999-11-09 | |
| | |||
* | Arrange for activate-scripting to not block for interactive calls. | 1999-11-09 | |
| | |||
* | Comments. | 1999-11-08 | |
| | |||
* | Typo. | 1999-11-08 | |
| | |||
* | Changed web page to official one. | 1999-11-08 | |
| | | | | Added x-symbol support (moved here from generic/proof-x-symbol) | ||
* | improved proof-shell-error-regexp; | 1999-10-29 | |
| | |||
* | isa-update-thy-only: 'try' option; | 1999-10-27 | |
| | |||
* | ProofGeneral.inform_file_processed/retracted; | 1999-10-26 | |
| | | | | improved proof-shell-compute-new-files-list (more robust); | ||
* | tuned proof-shell-error-regexp; | 1999-10-26 | |
| | |||
* | Changed name of proof-shell-cd-cmd for uniformity. | 1999-10-21 | |
| | |||
* | Add isa-shell-update-thy at the end of proof-activate-scripting-hook. | 1999-10-20 | |
| | |||
* | Added uncaught exception to error-regexp | 1999-10-19 | |
| | |||
* | Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic. | 1999-10-19 | |
| | |||
* | Deactivate scripting before retracting a theory file. Fix for DvO's report. | 1999-10-19 | |
| | |||
* | Whitespace | 1999-10-15 | |
| | |||
* | Fix for state-preserving-p | 1999-10-06 | |
| | |||
* | Made new command proof-cd to cd to the directory of the current | 1999-10-06 | |
| | | | | | | buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly. | ||
* | Turned off C-c C-l; fixed syntax for old result form; proof-showproof-command. | 1999-10-06 | |
| | |||
* | thy mode binding made to match with script mode | 1999-10-06 | |
| | |||
* | Renamed some configuration variables for uniformity, see CHANGES. | 1999-10-01 | |
| | |||
* | replaced isa-output-font-lock-terms by isa-output-font-lock-keywords-1; | 1999-09-30 | |
| | |||
* | Enabled hack for proof-shell-leave-annotations-in-output | 1999-09-29 | |
| | |||
* | Added setting for proof-find-theorems-command. | 1999-09-23 | |
| | |||
* | improved (?) proof-shell-proof-completed-regexp; | 1999-09-22 | |
| | |||
* | Adjusted proof-shell-proof-completed-regexp to match against whole of | 1999-09-21 | |
| | | | | | proofstate output including "No subgoals!" message. Now PG can correctly set the proof-shell-proof-completed flag. | ||
* | Maintainer addresses | 1999-08-23 | |
| | |||
* | fixed comment; | 1999-08-23 | |
| | |||
* | Added font-lock keywords and syntax table setup for buffers displaying | 1999-08-23 | |
| | | | | Isabelle output. | ||
* | eliminated superficial ';'s; | 1999-08-20 | |
| | |||
* | proof-shell-start-goals-regexp: include \n; | 1999-08-18 | |
| | | | | | isa-init-syntax-table moved to isa-syntax.el; improved isa-update-thy-only; | ||
* | proof-shell-first-special-char ?\350; | 1999-08-16 | |
| | | | | | | | | 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; | ||
* | renamed proof-commands-regexp to proof-indent-commands-regexp, which | 1999-05-27 | |
| | | | | is less confusing); | ||
* | fixed syntax entry for "_" | 1999-02-03 | |
| | |||
* | Regexp bug. Use proof-string-match appropriately. | 1999-02-01 | |
| | |||
* | Fixed broken check on proof-mode-hook. | 1998-12-15 | |
| | |||
* | made many minor changes to the documentation | 1998-12-15 | |
| | |||
* | Altered behaviour to allow retraction part-way through finished scripts. | 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). |