aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar.el
Commit message (Collapse)AuthorAge
* Set proof-shell-trace-output-regexp early enough to have effect. Fixes trac ↵Gravatar David Aspinall2008-01-29
| | | | #183, #186. See #190
* Add key binding for ML {* *} and fix longsuper, longsubGravatar David Aspinall2008-01-24
|
* Many compatibility updates, bug fixes, rearrangements for compilation.Gravatar David Aspinall2008-01-15
|
* Move x-symbol-isabelle -> x-symbol-isar to simplify setup.Gravatar David Aspinall2007-12-14
|
* Typo in pg-special-char-regexpGravatar David Aspinall2007-12-14
|
* Make value of pg-special-char-regexp depend on proof-shell-unicode.Gravatar David Aspinall2007-12-14
| | | | This makes sure that stripping special characters from output is accurate.
* proof-shell-issue-pgip-cmd is always isabelle-process-pgip;Gravatar Makarius Wenzel2007-10-24
|
* isar-find-and-forget: no special treatment of begin/end, just plain undoGravatar Makarius Wenzel2007-10-18
| | | | (in Isabelle2005 this will produce repeated errors after end-of-theory;
* allow more specials: oct 327 .. oct 340;Gravatar Makarius Wenzel2007-09-07
|
* pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing ↵Gravatar David Aspinall2007-08-19
| | | | markup (special 377).
* removed outated comment;Gravatar Makarius Wenzel2007-08-15
|
* isar-goalhyplit-test: explicit end-marker;Gravatar Makarius Wenzel2007-08-15
|
* Add support for sending back literal commands reusing PBP markup mechanisms.Gravatar David Aspinall2007-08-14
|
* reverted find theorems default from form to minibufferGravatar weber2007-06-11
|
* Rename [proof]find-theorems -> isar-find-theoremsGravatar David Aspinall2007-05-11
|
* Add experimental find theorems form (not working on all Emacs yet)Gravatar David Aspinall2007-05-10
|
* tuned cannot-undo;Gravatar Makarius Wenzel2007-05-08
|
* added isar-cmd-sledgehammer;Gravatar Makarius Wenzel2007-05-08
|
* tuned pg-special-char-regexp;Gravatar Makarius Wenzel2007-05-08
|
* Patch for XEmacs 21.5 beta match-replace bugGravatar David Aspinall2007-03-03
|
* Use Isar-specific isabelle-system fileGravatar David Aspinall2006-12-05
|
* isar-strip-terminators, isar-detect-begin: proof-search-forward;Gravatar Makarius Wenzel2006-11-04
|
* reintroduced pg-subterm-first-special-char, which makes PG strip goal markup;Gravatar Makarius Wenzel2006-10-11
| | | | | isar-find-and-forget: no special treatment of undo-kill, allows "context" command to act as local theory init;
* removed obsolete isar-detect-header;Gravatar Makarius Wenzel2006-10-11
| | | | isar-find-and-forget: proper handling of nested begin/end blocks;
* Changed the type of proof-goal-command-p. It takes now a span, whichGravatar Pierre Courtieu2006-04-26
| | | | | | allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
* isar-preprocessing: replace \n by \<^newline>;Gravatar Makarius Wenzel2006-02-12
|
* old specials are recogized again;Gravatar Makarius Wenzel2005-09-28
|
* Tweak.Gravatar David Aspinall2005-09-21
|
* Add command menuGravatar David Aspinall2005-09-21
|
* proof-shell-wakeup-char ?\^AGravatar Makarius Wenzel2005-09-17
|
* removed 8bit special chars for isar;Gravatar Makarius Wenzel2005-09-14
| | | | | removed unused Pbp setup; removed 'isabelle-convert-idmarkup-to-subterm, which expects 8bit specials;
* renamed thms_containing to find_theorems;Gravatar Makarius Wenzel2005-09-01
|
* special regexps: include PGASCII version;Gravatar Makarius Wenzel2005-09-01
| | | | pg-after-fontify-output-hook: always do pg-remove-specials;
* proof-defshortcut isar-local: \<^loc>;Gravatar Makarius Wenzel2005-08-26
|
* Fix isar-shell-adjust-line-width for mutliple frame mode.Gravatar David Aspinall2005-08-14
|
* next-error-regexp seems to have broken; fix it against current Isabelle CVS.Gravatar David Aspinall2005-08-09
|
* proof-defshortcut isar-bold;Gravatar Makarius Wenzel2005-08-08
|
* removed find_rwrites, print_intros;Gravatar Makarius Wenzel2005-05-22
|
* Changes from Clemens Ballarin for large X-Symbol fontsGravatar David Aspinall2005-02-15
|
* Remove print draft from menuGravatar David Aspinall2004-10-07
|
* Fix display_drafts -> print_draftsGravatar David Aspinall2004-07-23
|
* Fix index number back for isar-undo-remove-regexp, change isar-remove instead.Gravatar David Aspinall2004-06-17
|
* Fix error regexps for matching additional comma printed in position [NB: for ↵Gravatar David Aspinall2004-06-16
| | | | PGIP patched position.ML].
* Last change: added also isar-display-draft isar-print-draft forGravatar David Aspinall2004-06-16
| | | | repository versions of Isabelle.
* Fix for name matching changes grouping in isar-undo-remove-regexp.Gravatar David Aspinall2004-06-16
|
* Add functions for displaying/printing draft.Gravatar David Aspinall2004-06-13
|
* Set comment-quote-nested (for Emacs/XEmacs 21.5)Gravatar David Aspinall2004-05-09
|
* Patch from Brother MakariusGravatar David Aspinall2004-05-06
|
* Add shortcuts for new X-Symbol sequences.Gravatar David Aspinall2004-04-17
|
* Add proof-cannot-reopen-processed-files to fix behaviour of multiple files ↵Gravatar David Aspinall2004-04-17
| | | | for Isabelle.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 21:19:41 +0000