aboutsummaryrefslogtreecommitdiff
path: root/isar
AgeCommit message (Expand)Author
2008-01-30Harmonise a bit more with X-Symbols. Add customization facilityDavid Aspinall
2008-01-29isar-undos: fix bug trac #189 introduced by attempt to remove proof-no-command.David Aspinall
2008-01-29Set proof-shell-trace-output-regexp early enough to have effect. Fixes trac ...David Aspinall
2008-01-28Switch to fake long symbolsDavid Aspinall
2008-01-28Prevent prompt during compilationDavid Aspinall
2008-01-28Add hooks for unicode tokens within proof shellDavid Aspinall
2008-01-28Add shortcuts for tokens.David Aspinall
2008-01-27Switch token table mapping destination from glyph names to unicode strings. ...David Aspinall
2008-01-25fixed usage: default for option -p is emacs, not xemacs;Makarius Wenzel
2008-01-25Fix previous change.David Aspinall
2008-01-25Make isatool usage (view doc) compatible with proof-rsh-command.David Aspinall
2008-01-25Make isatool usage compatible with proof-rsh-command.David Aspinall
2008-01-25New files.David Aspinall
2008-01-24Remove use of proof-assDavid Aspinall
2008-01-24Add key binding for ML {* *} and fix longsuper, longsubDavid Aspinall
2008-01-16Updated.David Aspinall
2008-01-16Updated.David Aspinall
2008-01-15Default to using emacs nowDavid Aspinall
2008-01-15Many compatibility updates, bug fixes, rearrangements for compilation.David Aspinall
2007-12-14Move x-symbol-isabelle -> x-symbol-isar to simplify setup.David Aspinall
2007-12-14Deleted fileDavid Aspinall
2007-12-14Typo in pg-special-char-regexpDavid Aspinall
2007-12-14x-symbol-isabelle-prepare-table: specialise to Isar (usefully removes depende...David Aspinall
2007-12-14Remove eval-when, seems unreliableDavid Aspinall
2007-12-14Improve loading; these tests are not functioning yetDavid Aspinall
2007-12-14Make value of pg-special-char-regexp depend on proof-shell-unicode.David Aspinall
2007-12-13Cleanup. Add more insertion commands.David Aspinall
2007-12-13Deleted fileDavid Aspinall
2007-12-09Comment unused functionDavid Aspinall
2007-11-20clarify that -U now defaults to true;Makarius Wenzel
2007-11-13command 'thm' makes no sense outside a proper context;Makarius Wenzel
2007-11-12VersionsDavid Aspinall
2007-10-24proof-shell-issue-pgip-cmd is always isabelle-process-pgip;Makarius Wenzel
2007-10-24removed obsolete isabelle-version-string, isa-version, isa-supports-pgip;Makarius Wenzel
2007-10-18isar-find-and-forget: no special treatment of begin/end, just plain undoMakarius Wenzel
2007-10-18isar-undo-fail-regexp: only isar-keywords-control, not isar-keywords-theory-end;Makarius Wenzel
2007-09-07allow more specials: oct 327 .. oct 340;Makarius Wenzel
2007-09-07isar-output-font-lock-keywords-1: hilite markup uses proof-warning-face;Makarius Wenzel
2007-08-19pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing mark...David Aspinall
2007-08-15removed outated comment;Makarius Wenzel
2007-08-15isar-goalhyplit-test: explicit end-marker;Makarius Wenzel
2007-08-14Add support for sending back literal commands reusing PBP markup mechanisms.David Aspinall
2007-06-14isar-improper-regexp: include "prems";Makarius Wenzel
2007-06-14single-char-regexp: tuned symbol regexp;Makarius Wenzel
2007-06-14isar-font-lock-local: tuned symbol regexp;Makarius Wenzel
2007-06-11reverted find theorems default from form to minibufferweber
2007-05-17XEmacs 21.4.15 does not seem to know propertizeweber
2007-05-11Fix renameweber
2007-05-11Fix renameweber
2007-05-11works with XEmacs now (ticket #115)weber
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:32:26 +0000