aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa
Commit message (Collapse)AuthorAge
...
* Fixed up proof-shell-proof-completed mess nicely.Gravatar David Aspinall2000-04-07
|
* tuned \<bottom>;Gravatar Makarius Wenzel2000-04-06
| | | | added \<lbrace>, \<rbrace>, \<top>;
* tuned todo stuff;Gravatar Makarius Wenzel2000-04-05
|
* improved print_mode switch;Gravatar Makarius Wenzel2000-04-05
|
* Added provisional commands for enabling/disabling printing.Gravatar David Aspinall2000-04-04
|
* Save as Example.ML, except using X-Symbol input tokens.Gravatar David Aspinall2000-04-04
|
* Fix accidently introduced bug with passing full paths to theory loader.Gravatar David Aspinall2000-04-04
|
* Removed pg_saved_gl which was for testing.Gravatar David Aspinall2000-03-24
|
* Do need to strip drive name as Jacques discovered.Gravatar David Aspinall2000-03-24
|
* Fix name of win32-long-file-name used as check.Gravatar David Aspinall2000-03-24
|
* Quoted backslashes.Gravatar David Aspinall2000-03-24
|
* Sensible default for Windows invoking IsabelleGravatar David Aspinall2000-03-24
|
* Attempt to fix filename mess for Windows.Gravatar David Aspinall2000-03-24
|
* Updated Isabelle home page.Gravatar David Aspinall2000-03-23
|
* Switch back to %s, rename proof-shell-string-escapes -> ↵Gravatar David Aspinall2000-03-22
| | | | proof-shell-filename-escapes, and always apply for filename substn.
* Fix other file commands to use %e substitution.Gravatar David Aspinall2000-03-22
|
* Use new format character %s to %e to cope with nasty filenames with backslashes.Gravatar David Aspinall2000-03-22
|
* transparent cd;Gravatar Makarius Wenzel2000-03-22
|
* Added settings for silent control.Gravatar David Aspinall2000-03-19
|
* New/updated information filesGravatar David Aspinall2000-03-13
|
* DocstringsGravatar David Aspinall2000-03-10
|
* Added menu item to switch to script buffer, C-c C-o key.Gravatar David Aspinall2000-03-10
|
* Updated headers.Gravatar David Aspinall2000-03-09
|
* UpdatedGravatar David Aspinall2000-03-09
|
* Added README files for each prover, summarizing status.Gravatar David Aspinall2000-03-09
|
* Split low-level todo into several files.Gravatar David Aspinall2000-03-08
|
* tuned electric-ignore;Gravatar Makarius Wenzel2000-02-23
|
* fix electric-ignore (due to DvO);Gravatar Makarius Wenzel2000-02-15
|
* option -x: enable x-symbol package;Gravatar Makarius Wenzel2000-02-11
|
* setup proof-shell-pre-interrupt-hook for Poly/ML;Gravatar Makarius Wenzel2000-02-10
|
* fixed proof-shell-error-regexp;Gravatar Makarius Wenzel2000-02-07
|
* CommentsGravatar David Aspinall2000-01-12
|
* Fixes for short output duplication problem: set ↵Gravatar David Aspinall2000-01-06
| | | | proof-shell-eager-annotation-start-length.
* Change SML minor mode binding to C-c C-m, avoiding clash withGravatar David Aspinall1999-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 modeGravatar David Aspinall1999-11-29
|
* Fix to proof-shell-proof-completed-regexp by reverting to previous version.Gravatar David Aspinall1999-11-26
|
* Made thy-indent-level a user opt.Gravatar David Aspinall1999-11-24
|
* Patch to proof-shell-proof-completed-regexp to prevent overflow, sent by MarkusGravatar David Aspinall1999-11-23
|
* tuned faces;Gravatar Makarius Wenzel1999-11-22
|
* Added by defvars x-symbol-isa-name, x-symbol-isa-modeline-name so can use ↵Gravatar David Aspinall1999-11-19
| | | | this file without PG
* Failed attempt to trap C-g during try-update-thy. Left as comments.Gravatar David Aspinall1999-11-18
|
* Remove some obsolete/unecessary stuff.Gravatar David Aspinall1999-11-17
|
* Cleanups and a bit more highlightingGravatar David Aspinall1999-11-16
|
* Matching goals regexp. Comments.Gravatar David Aspinall1999-11-16
|
* Removed font-lock settings. Set proof-font-lock-zap-commas=tGravatar David Aspinall1999-11-15
|
* Many robustness improvements for error and interrupt handling:Gravatar David Aspinall1999-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 highlightingGravatar David Aspinall1999-11-14
|
* proof-nested-goals-allowed -> proof-completed-proof-behaviourGravatar David Aspinall1999-11-14
| | | | | Patch for more flexible handling of closing goal...save regions after proof has been completed.
* More theory file sectionsGravatar David Aspinall1999-11-12
|
* Fixes for Isabelle in case theory file is visited before script file.Gravatar David Aspinall1999-11-12
|