| Age | Commit message (Collapse) | Author |
|---|
|
|
|
- remove visibility specs and script portion records during undo
- clear visibility specs on restart
|
|
'goalsave again. Add idiom property.
|
|
suggested by Markus
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix bug in proof-goto-end-of-locked.
|
|
|
|
|
|
|
|
|
|
|
|
Tweaks to proof-script-generic-parse-cmdstart. Combine fly-past and coelesce comment options. Use proof-string-match-safe in generic-goal-command-p, to avoid error in Twelf.
|
|
|
|
Make toolbar commands work from non-scripting buffers
Add save file dialogue to proof-register-possibly-new-processed-file
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
