| Age | Commit message (Collapse) | Author |
|---|
|
|
|
proof-xxx-with-hole-regexp
|
|
|
|
|
|
|
|
safe default of empty string (now will have error msgs from filter)
|
|
|
|
|
|
|
|
|
|
new parsing functions.
|
|
replaced spurious re-search-forward by proof-re-search-forward;
proof-script-important-settings: commented out proof-goal-with-hole-regexp,
proof-save-with-hole-regexp;
|
|
|
|
|
|
|
|
|
|
prefix and comment/string (e.g. { vs {* in Isar);
|
|
if already set.
|
|
Select new parsing function according to config variables
Use proof-comment-{start,end}-regexp, and set default values
in proof-config-done-related, from proof-comment-{start,end}
New proof-script-complete which uses proof-case-fold-search
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Comments about failure for ;;;###autoload cookie for define-derived-mode
Attempted fixes for C-x C-w, C-x C-v, revert-buffer.
|
|
|
|
|
|
proof-follow-mode='ignore
|
|
|
|
|
|
|
|
more efficient, also works around crash bug in xemacs-21.1.7/SuSE);
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof-undo-and-delete-last-successful-command.
|
|
|
|
|
|
|
|
|
|
|
|
|
