Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add universal keys to theory mode | David Aspinall | 1999-11-29 |
| | |||
* | Fix to proof-shell-proof-completed-regexp by reverting to previous version. | David Aspinall | 1999-11-26 |
| | |||
* | Made thy-indent-level a user opt. | David Aspinall | 1999-11-24 |
| | |||
* | Patch to proof-shell-proof-completed-regexp to prevent overflow, sent by Markus | David Aspinall | 1999-11-23 |
| | |||
* | tuned faces; | Makarius Wenzel | 1999-11-22 |
| | |||
* | Added by defvars x-symbol-isa-name, x-symbol-isa-modeline-name so can use ↵ | David Aspinall | 1999-11-19 |
| | | | | this file without PG | ||
* | Failed attempt to trap C-g during try-update-thy. Left as comments. | David Aspinall | 1999-11-18 |
| | |||
* | Remove some obsolete/unecessary stuff. | David Aspinall | 1999-11-17 |
| | |||
* | Cleanups and a bit more highlighting | David Aspinall | 1999-11-16 |
| | |||
* | Matching goals regexp. Comments. | David Aspinall | 1999-11-16 |
| | |||
* | Removed font-lock settings. Set proof-font-lock-zap-commas=t | David Aspinall | 1999-11-15 |
| | |||
* | Many robustness improvements for error and interrupt handling: | David Aspinall | 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) | ||
* | More highlighting | David Aspinall | 1999-11-14 |
| | |||
* | proof-nested-goals-allowed -> proof-completed-proof-behaviour | David Aspinall | 1999-11-14 |
| | | | | | Patch for more flexible handling of closing goal...save regions after proof has been completed. | ||
* | More theory file sections | David Aspinall | 1999-11-12 |
| | |||
* | Fixes for Isabelle in case theory file is visited before script file. | David Aspinall | 1999-11-12 |
| | |||
* | Display qed message in goals buffer | David Aspinall | 1999-11-12 |
| | |||
* | Next round of fixups for font-lock and x-symbol. | David Aspinall | 1999-11-11 |
| | |||
* | Extensive fixes for x-symbol and font-lock. | David Aspinall | 1999-11-11 |
| | |||
* | Removed unsociable key-bindings. | David Aspinall | 1999-11-10 |
| | |||
* | Fixes for x-symbol activation/deactivation strings | David Aspinall | 1999-11-09 |
| | |||
* | Arrange for activate-scripting to not block for interactive calls. | David Aspinall | 1999-11-09 |
| | |||
* | Comments. | David Aspinall | 1999-11-08 |
| | |||
* | Typo. | David Aspinall | 1999-11-08 |
| | |||
* | Changed web page to official one. | David Aspinall | 1999-11-08 |
| | | | | Added x-symbol support (moved here from generic/proof-x-symbol) | ||
* | improved proof-shell-error-regexp; | Makarius Wenzel | 1999-10-29 |
| | |||
* | isa-update-thy-only: 'try' option; | Makarius Wenzel | 1999-10-27 |
| | |||
* | ProofGeneral.inform_file_processed/retracted; | Makarius Wenzel | 1999-10-26 |
| | | | | improved proof-shell-compute-new-files-list (more robust); | ||
* | tuned proof-shell-error-regexp; | Makarius Wenzel | 1999-10-26 |
| | |||
* | isa-keywords-save: removed "result"; | Makarius Wenzel | 1999-10-26 |
| | | | | | | isa-keywords-commands: added "ProofGeneral.repeat_undo"; added isa-keywords-proof-commands; added isa-verbatim; | ||
* | update by DvO; | Makarius Wenzel | 1999-10-22 |
| | |||
* | Changed name of proof-shell-cd-cmd for uniformity. | David Aspinall | 1999-10-21 |
| | |||
* | Add isa-shell-update-thy at the end of proof-activate-scripting-hook. | David Aspinall | 1999-10-20 |
| | |||
* | Added uncaught exception to error-regexp | David Aspinall | 1999-10-19 |
| | |||
* | Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic. | David Aspinall | 1999-10-19 |
| | |||
* | Deactivate scripting before retracting a theory file. Fix for DvO's report. | David Aspinall | 1999-10-19 |
| | |||
* | Whitespace | David Aspinall | 1999-10-15 |
| | |||
* | let PROOFGENERAL_ASSISTANTS control isa vs. isar selection; | Makarius Wenzel | 1999-10-15 |
| | |||
* | Fix for state-preserving-p | David Aspinall | 1999-10-06 |
| | |||
* | Made new command proof-cd to cd to the directory of the current | David Aspinall | 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. | David Aspinall | 1999-10-06 |
| | |||
* | thy mode binding made to match with script mode | David Aspinall | 1999-10-06 |
| | |||
* | Renamed some configuration variables for uniformity, see CHANGES. | David Aspinall | 1999-10-01 |
| | |||
* | replaced isa-output-font-lock-terms by isa-output-font-lock-keywords-1; | Makarius Wenzel | 1999-09-30 |
| | |||
* | tuned isa-init-output-syntax-table; | Makarius Wenzel | 1999-09-30 |
| | | | | | | removed isa-binder-regexp (obsolete); remove isa-font-lock-terms; proper isa-output-font-lock-keywords-1; | ||
* | Enabled hack for proof-shell-leave-annotations-in-output | David Aspinall | 1999-09-29 |
| | |||
* | Added setting for proof-find-theorems-command. | David Aspinall | 1999-09-23 |
| | |||
* | tuned example according to Isabelle style-guide; | Makarius Wenzel | 1999-09-22 |
| | |||
* | improved (?) proof-shell-proof-completed-regexp; | Makarius Wenzel | 1999-09-22 |
| | |||
* | Fix for proof-shell-proof-completed-regexp | David Aspinall | 1999-09-21 |
| |