Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Comment unused function | 2007-12-09 | |
| | |||
* | clarify that -U now defaults to true; | 2007-11-20 | |
| | |||
* | command 'thm' makes no sense outside a proper context; | 2007-11-13 | |
| | | | | fixed spelling; | ||
* | Versions | 2007-11-12 | |
| | |||
* | proof-shell-issue-pgip-cmd is always isabelle-process-pgip; | 2007-10-24 | |
| | |||
* | removed obsolete isabelle-version-string, isa-version, isa-supports-pgip; | 2007-10-24 | |
| | |||
* | isar-find-and-forget: no special treatment of begin/end, just plain undo | 2007-10-18 | |
| | | | | (in Isabelle2005 this will produce repeated errors after end-of-theory; | ||
* | isar-undo-fail-regexp: only isar-keywords-control, not isar-keywords-theory-end; | 2007-10-18 | |
| | |||
* | allow more specials: oct 327 .. oct 340; | 2007-09-07 | |
| | |||
* | isar-output-font-lock-keywords-1: hilite markup uses proof-warning-face; | 2007-09-07 | |
| | |||
* | pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing ↵ | 2007-08-19 | |
| | | | | markup (special 377). | ||
* | removed outated comment; | 2007-08-15 | |
| | |||
* | isar-goalhyplit-test: explicit end-marker; | 2007-08-15 | |
| | |||
* | Add support for sending back literal commands reusing PBP markup mechanisms. | 2007-08-14 | |
| | |||
* | isar-improper-regexp: include "prems"; | 2007-06-14 | |
| | | | | Cvs: ---------------------------------------------------------------------- | ||
* | single-char-regexp: tuned symbol regexp; | 2007-06-14 | |
| | | | | subscript-matcher: more robust handling of non-space lookahead (beware of markuo specials!); | ||
* | isar-font-lock-local: tuned symbol regexp; | 2007-06-14 | |
| | |||
* | reverted find theorems default from form to minibuffer | 2007-06-11 | |
| | |||
* | XEmacs 21.4.15 does not seem to know propertize | 2007-05-17 | |
| | |||
* | Fix rename | 2007-05-11 | |
| | |||
* | Fix rename | 2007-05-11 | |
| | |||
* | works with XEmacs now (ticket #115) | 2007-05-11 | |
| | |||
* | Fix rename | 2007-05-11 | |
| | |||
* | Rename [proof]find-theorems -> isar-find-theorems | 2007-05-11 | |
| | |||
* | Renamed file | 2007-05-11 | |
| | |||
* | Add experimental find theorems form (not working on all Emacs yet) | 2007-05-10 | |
| | |||
* | New files. | 2007-05-10 | |
| | |||
* | x-symbol-isabelle-font-lock-regexp: demand subsequent non-space character; | 2007-05-08 | |
| | |||
* | undo: removed confusing comment; | 2007-05-08 | |
| | |||
* | tuned cannot-undo; | 2007-05-08 | |
| | |||
* | added isar-cmd-sledgehammer; | 2007-05-08 | |
| | |||
* | tuned pg-special-char-regexp; | 2007-05-08 | |
| | |||
* | Patch for XEmacs 21.5 beta match-replace bug | 2007-03-03 | |
| | |||
* | Fix comment | 2007-02-28 | |
| | |||
* | Comment about undo; use | 2007-01-10 | |
| | |||
* | tuned; | 2006-12-30 | |
| | |||
* | back again for isar; | 2006-12-07 | |
| | |||
* | isar-keywords-theory-enclose: isar-keywords-theory-switch is back again (in ↵ | 2006-12-07 | |
| | | | | post-Isabelle2005 the latter is empty anyway); | ||
* | removed obsolete references to 'isa'; | 2006-12-07 | |
| | |||
* | proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which ↵ | 2006-12-07 | |
| | | | | breaks Poly/MK 5; | ||
* | X-Symbol config. Moved from isa/ | 2006-12-05 | |
| | |||
* | Use Isar-specific isabelle-system file | 2006-12-05 | |
| | |||
* | isar-keywords-theory-enclose: removed isar-keywords-theory-switch, which ↵ | 2006-11-04 | |
| | | | | | | | usually appears locally as plain theory command; isar-keywords-proper: simplified font-lock; added isar-match-nesting -- distinguishes font-lock for local vs. global begin/end; | ||
* | isar-strip-terminators, isar-detect-begin: proof-search-forward; | 2006-11-04 | |
| | |||
* | reintroduced pg-subterm-first-special-char, which makes PG strip goal markup; | 2006-10-11 | |
| | | | | | isar-find-and-forget: no special treatment of undo-kill, allows "context" command to act as local theory init; | ||
* | isar-keywords-indent-enclose: include "begin" keyword; | 2006-10-11 | |
| | | | | removed obsolete kill/undo-kill-regexp; | ||
* | added regexps for begin/end and theory start; | 2006-10-11 | |
| | |||
* | removed obsolete isar-detect-header; | 2006-10-11 | |
| | | | | isar-find-and-forget: proper handling of nested begin/end blocks; | ||
* | isar-goals-font-lock-keywords: added abbreviations; | 2006-08-16 | |
| | |||
* | Changed the type of proof-goal-command-p. It takes now a span, which | 2006-04-26 | |
| | | | | | | allows using a span attribute to detect goal commands. I think I modified all modes accordingly. |