proof-general - Emacs interface for proof assistants

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