aboutsummaryrefslogtreecommitdiff
path: root/isar/isar.el
AgeCommit message (Expand)Author
2009-09-04Add option to do command wrappingDavid Aspinall
2009-09-04Remove proof-shell-prompt-pattern, no longer used.David Aspinall
2009-09-04Remove proof-no-commandDavid Aspinall
2009-08-31Doc fixesDavid Aspinall
2009-08-31Prevent reporting column number back to Isabelle processDavid Aspinall
2009-08-31Quick fix to isar-remove-file, see trac #274David Aspinall
2009-08-29isar-positions-of: skip whitespace before command startDavid Aspinall
2009-08-28isar-nonwrap-regexp: ML should work (note that there are *many* ML commands);Makarius Wenzel
2009-08-28Fix compile warningsDavid Aspinall
2009-08-28CommentsDavid Aspinall
2009-08-25Add menu entry for setting proof assistant commandDavid Aspinall
2009-08-19Enhance command markup to pass position information. Extend defaults for res...David Aspinall
2009-08-18Hints about setting position in commandDavid Aspinall
2009-08-18First attempt at command wrapping (see http://proofgeneral.inf.ed.ac.uk/trac/...David Aspinall
2009-08-17TidyDavid Aspinall
2009-08-14Set proof-query-identifier-command in right place.David Aspinall
2009-08-07Rename proof-shell-identifier-under-mouse-cmd -> proof-query-identifier-commandDavid Aspinall
2009-08-06Add configuration setting for Find Theorems formDavid Aspinall
2009-05-26Set strip-output-function for pasting. Adjust font-lock handling toDavid Aspinall
2009-05-26Add proof-electric-terminator-noterminator behaviour for IsarDavid Aspinall
2009-05-26Rename isatool -> isabelleDavid Aspinall
2009-03-31eliminated obsolete non-ASCII specials;Makarius Wenzel
2008-07-24Merge changes from Version4Branch.David Aspinall
2008-07-10Use proof-guess-command-line to adjust command line when starting Isabelle.David Aspinall
2008-07-10Start to rationalise setting for proof-prog-name.David Aspinall
2008-02-17Remove isar-activate-scripting, which was identical to defaultDavid Aspinall
2008-02-17Set proof-shell-eager-annotation-start-length=2. This should have beenDavid Aspinall
2008-02-04Add mode documentationDavid Aspinall
2008-01-29Set proof-shell-trace-output-regexp early enough to have effect. Fixes trac ...David Aspinall
2008-01-24Add key binding for ML {* *} and fix longsuper, longsubDavid 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-14Typo in pg-special-char-regexpDavid Aspinall
2007-12-14Make value of pg-special-char-regexp depend on proof-shell-unicode.David Aspinall
2007-10-24proof-shell-issue-pgip-cmd is always isabelle-process-pgip;Makarius Wenzel
2007-10-18isar-find-and-forget: no special treatment of begin/end, just plain undoMakarius Wenzel
2007-09-07allow more specials: oct 327 .. oct 340;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-11reverted find theorems default from form to minibufferweber
2007-05-11Rename [proof]find-theorems -> isar-find-theoremsDavid Aspinall
2007-05-10Add experimental find theorems form (not working on all Emacs yet)David Aspinall
2007-05-08tuned cannot-undo;Makarius Wenzel
2007-05-08added isar-cmd-sledgehammer;Makarius Wenzel
2007-05-08tuned pg-special-char-regexp;Makarius Wenzel
2007-03-03Patch for XEmacs 21.5 beta match-replace bugDavid Aspinall
2006-12-05Use Isar-specific isabelle-system fileDavid Aspinall
2006-11-04isar-strip-terminators, isar-detect-begin: proof-search-forward;Makarius Wenzel