| Age | Commit message (Collapse) | Author |
|---|
|
|
|
off minor modes in buffers automatically. Now the PG setting controls
the "default global for PG buffers" for each of these. The menu
checkbox simply displays the current minor mode status. When this
is changed, the PG global mode follows suit. We do not try to
apply the change to all PG buffers (30 minutes of fontification!).
|
|
|
|
|
|
|
|
|
|
|
|
Monnier
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
autosave case.
|
|
|
|
|
|
|
|
proof-script-comment-{start,end}-regexp.
|
|
|
|
|
|
|
|
|
|
|
|
rather than always retracting.
|
|
|
|
|
|
|
|
proof-nested-goals-history.
|
|
for all retraction.
|
|
|
|
|
|
behaviour for Isar). Isar goal/save regexps dont match up properly.
|
|
|
|
proof-done-advancing.
|
|
|
|
determination/reporting. Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings
|
|
|
|
|
|
|
|
|
|
to control spans.
|
|
|
|
Use new functions pg-set-span-helphighlights and pg-span-name
to set help echo, balloon help, mouse highlight, and context
menu.
|
|
|
|
Added 'controlspan property to proof body spans: action will be
controlled from the control span. (The 'goalsave is the parent).
Replace 'highlight face with 'proof-mouse-highlight-face throughout.
|
|
|
|
proofbodyspan;
handle proof-script-integral-proofs;
|
|
on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated
|
