Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Fixed up proof-shell-proof-completed mess nicely. | 2000-04-07 | ||
| | ||||
* | tuned \<bottom>; | 2000-04-06 | ||
| | | | | added \<lbrace>, \<rbrace>, \<top>; | |||
* | tuned todo stuff; | 2000-04-05 | ||
| | ||||
* | improved print_mode switch; | 2000-04-05 | ||
| | ||||
* | Added provisional commands for enabling/disabling printing. | 2000-04-04 | ||
| | ||||
* | Save as Example.ML, except using X-Symbol input tokens. | 2000-04-04 | ||
| | ||||
* | Fix accidently introduced bug with passing full paths to theory loader. | 2000-04-04 | ||
| | ||||
* | Removed pg_saved_gl which was for testing. | 2000-03-24 | ||
| | ||||
* | Do need to strip drive name as Jacques discovered. | 2000-03-24 | ||
| | ||||
* | Fix name of win32-long-file-name used as check. | 2000-03-24 | ||
| | ||||
* | Quoted backslashes. | 2000-03-24 | ||
| | ||||
* | Sensible default for Windows invoking Isabelle | 2000-03-24 | ||
| | ||||
* | Attempt to fix filename mess for Windows. | 2000-03-24 | ||
| | ||||
* | Updated Isabelle home page. | 2000-03-23 | ||
| | ||||
* | Switch back to %s, rename proof-shell-string-escapes -> ↵ | 2000-03-22 | ||
| | | | | proof-shell-filename-escapes, and always apply for filename substn. | |||
* | Fix other file commands to use %e substitution. | 2000-03-22 | ||
| | ||||
* | Use new format character %s to %e to cope with nasty filenames with backslashes. | 2000-03-22 | ||
| | ||||
* | transparent cd; | 2000-03-22 | ||
| | ||||
* | Added settings for silent control. | 2000-03-19 | ||
| | ||||
* | New/updated information files | 2000-03-13 | ||
| | ||||
* | Docstrings | 2000-03-10 | ||
| | ||||
* | Added menu item to switch to script buffer, C-c C-o key. | 2000-03-10 | ||
| | ||||
* | Updated headers. | 2000-03-09 | ||
| | ||||
* | Updated | 2000-03-09 | ||
| | ||||
* | Added README files for each prover, summarizing status. | 2000-03-09 | ||
| | ||||
* | Split low-level todo into several files. | 2000-03-08 | ||
| | ||||
* | tuned electric-ignore; | 2000-02-23 | ||
| | ||||
* | fix electric-ignore (due to DvO); | 2000-02-15 | ||
| | ||||
* | option -x: enable x-symbol package; | 2000-02-11 | ||
| | ||||
* | setup proof-shell-pre-interrupt-hook for Poly/ML; | 2000-02-10 | ||
| | ||||
* | fixed proof-shell-error-regexp; | 2000-02-07 | ||
| | ||||
* | Comments | 2000-01-12 | ||
| | ||||
* | Fixes for short output duplication problem: set ↵ | 2000-01-06 | ||
| | | | | proof-shell-eager-annotation-start-length. | |||
* | Change SML minor mode binding to C-c C-m, avoiding clash with | 1999-11-29 | ||
| | | | | | proof-interrupt-process. Add commands from proof-universal-keys to menu, and add all of proof-shared-menu. | |||
* | Add universal keys to theory mode | 1999-11-29 | ||
| | ||||
* | Fix to proof-shell-proof-completed-regexp by reverting to previous version. | 1999-11-26 | ||
| | ||||
* | Made thy-indent-level a user opt. | 1999-11-24 | ||
| | ||||
* | Patch to proof-shell-proof-completed-regexp to prevent overflow, sent by Markus | 1999-11-23 | ||
| | ||||
* | tuned faces; | 1999-11-22 | ||
| | ||||
* | Added by defvars x-symbol-isa-name, x-symbol-isa-modeline-name so can use ↵ | 1999-11-19 | ||
| | | | | this file without PG | |||
* | 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) | |||
* | More highlighting | 1999-11-14 | ||
| | ||||
* | 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. | |||
* | More theory file sections | 1999-11-12 | ||
| | ||||
* | Fixes for Isabelle in case theory file is visited before script file. | 1999-11-12 | ||
| |