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