aboutsummaryrefslogtreecommitdiff
path: root/generic
AgeCommit message (Collapse)Author
2001-09-04Nested proof spans are duplicableDavid Aspinall
2001-09-04Add experimental features settingDavid Aspinall
2001-09-03Change colour of locked region.David Aspinall
2001-09-03Fix bracket bug.David Aspinall
2001-09-03Show/hide all proofs: add redisplay for FSFDavid Aspinall
Use new functions pg-set-span-helphighlights and pg-span-name to set help echo, balloon help, mouse highlight, and context menu.
2001-09-03Use pg-set-span-helphightlights for unhighlighting.David Aspinall
2001-09-03Generalise context menu for other spans; grey out show/hide when unavailable.David Aspinall
2001-09-03Set version tag for new release.David Aspinall
2001-09-03FormattingDavid Aspinall
2001-09-03Add specific install instrs, rearrange.David Aspinall
2001-09-03Added handling of tracing buffers using proof-shell-spill-output-regexp.David Aspinall
2001-09-03Added proof-shell-spill-output-regexpDavid Aspinall
2001-09-02Set version tag for new release.David Aspinall
2001-08-31(Almost) complete rewriteDavid Aspinall
2001-08-31UpdatedDavid Aspinall
2001-08-31Move theorem dependency code into proof-depends.el.David Aspinall
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.
2001-08-31Added copy command, call to dependency menu if proof-depends is loaded.David Aspinall
2001-08-31Add new proof-mouse-highlight-face to use instead of default. Fix ↵David Aspinall
dependency faces.
2001-08-31Add faces for theorem dependencies.David Aspinall
2001-08-31Clean up of proof-dependsDavid Aspinall
2001-08-31Skip settings which have no PA command in proof-assistant-settings-cmdDavid Aspinall
2001-08-31Add proof-shell-kill-function-hooksDavid Aspinall
2001-08-30pg-add-proof-element: removed accidential (?) dynamic scoping onMakarius Wenzel
proofbodyspan; handle proof-script-integral-proofs;
2001-08-30added proof-script-integral-proofs ("Whether the complete text after aMakarius Wenzel
goal confines the actual proof.");
2001-08-30Set version tag for new release.David Aspinall
2001-08-30Add reassurance to interrupt warning to make Markus happier.David Aspinall
2001-08-30Updates for recent version of X-symbol, which has no file called ↵David Aspinall
x-symbol-autoloads.
2001-08-30Add :eval form for defpacustom to define PA-specific PG settings as well as ↵David Aspinall
PA settings.
2001-08-30Add variable proof-previous-script-bufferDavid Aspinall
2001-08-30fixes for FSF Emacs for searching for goal span (don't call goal-command-p ↵David Aspinall
on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated
2001-08-30Added implementation of remassq for FSF EmacsDavid Aspinall
2001-08-30pg-insert-last-output-as-comment strips special annotations from last output ↵David Aspinall
before inserting as comment.
2001-08-28Set version tag for new release.David Aspinall
2001-08-28Change of proof span type back to goalsave fixDavid Aspinall
2001-08-28Remove dependent setting of timeout, since bin calls different fn now.David Aspinall
2001-08-28TrivialDavid Aspinall
2001-08-28Remove mention of toolbar variable. Make timeouts vary according to how ↵David Aspinall
started.
2001-08-28Timeout happens as intended now, while loading some parts of PG.David Aspinall
2001-08-17Set version tag for new release.David Aspinall
2001-08-17Trim visibility implementation:David Aspinall
- remove visibility specs and script portion records during undo - clear visibility specs on restart
2001-08-17Add span-delete-action hookDavid Aspinall
2001-08-17Fix bug in proof-display-and-keep-buffer which had resulted in switching ↵David Aspinall
minibuffer windows buffer.
2001-08-16Set version tag for new release.David Aspinall
2001-08-16Switch back to using goalsave spans in PBP codeDavid Aspinall
2001-08-16Add hide/show commands instead of make proofs visibleDavid Aspinall
2001-08-16Generate intermediate proof span for contents of proof; other becomes ↵David Aspinall
'goalsave again. Add idiom property.
2001-08-16Function name fixes, use idiom property in span for popup menu name.David Aspinall
2001-08-10Use proof-looking-at-syntactic-context function from proof-syntax, as ↵David Aspinall
suggested by Markus
2001-08-10Found another instance of buffer-syntactic-contextDavid Aspinall
2001-08-10Set version tag for new release.David Aspinall