proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Comments	David Aspinall	2002-08-31
\|
*	Patch from Stefan Monnier for using nested-comment aware parser on GNU Emacs.	David Aspinall	2002-08-30
\|
*	Imenu addition, layout fixes, from Stefan Monnier	David Aspinall	2002-08-29
\|
*	checkdoc induced docstring tweaks.	David Aspinall	2002-08-28
\|
*	Make font-lock-keywords buffer local for sake of Emacs 21.2.	David Aspinall	2002-08-28
\|
*	Doc	David Aspinall	2002-08-09
\|
*	Fix proof-disappearing-proofs; comments	David Aspinall	2002-08-09
\|
*	Refactor proof-done-advancing by abstracting out new functions; fixes for ↵	David Aspinall	2002-08-09
\| \| \| \|	autosave case.
*	Generalise proof elements to include comments, show/hiding of comments.	David Aspinall	2002-08-08
\|
*	Prevent proof spans being duplicated.	David Aspinall	2002-08-08
\|
*	Use glyph for hidden proofs; add open isearch props; tweak element handling fns.	David Aspinall	2002-08-08
\|
*	Variable name change proof-comment-{start,end}-regexp -> ↵	David Aspinall	2002-07-19
\| \| \| \|	proof-script-comment-{start,end}-regexp.
*	Add note about proof-generic-state-preserving-p	David Aspinall	2002-07-17
\|
*	Cleanups	David Aspinall	2002-07-17
\|
*	condition-case -> ignore-errors, comment.	David Aspinall	2002-07-12
\|
*	proof-restart: also remove idiom internal spans.	David Aspinall	2002-07-01
\|
*	Fix error catching in proof-deactivate-scripting-auto.	David Aspinall	2002-06-30
\|
*	When killing process or scripting buffer, register file if it is complete, ↵	David Aspinall	2002-06-30
\| \| \| \|	rather than always retracting.
*	use-old-parser setting replaces use-new-parser setting [WARNING: big change]	David Aspinall	2002-06-24
\|
*	GPL	David Aspinall	2002-06-21
\|
*	Remove lift-global function.	David Aspinall	2002-06-18
\|
*	Remove global testing and lift-global function; rename proof-nested-goals -> ↵	David Aspinall	2002-06-18
\| \| \| \|	proof-nested-goals-history.
*	A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ↵	David Aspinall	2002-06-13
\| \| \| \|	for all retraction.
*	Adjust proof-nesting depth, add FIXME notes since not right yet	David Aspinall	2002-06-12
\|
*	Add nestedundos setting to span, and proof-nested-undo-regexp setting	David Aspinall	2002-06-12
\|
*	Only match saves for prover that supports nested proofs (restores old ↵	David Aspinall	2002-06-11
\| \| \| \|	behaviour for Isar). Isar goal/save regexps dont match up properly.
*	Improved proof-nesting-depth (not finished yet)	David Aspinall	2002-06-11
\|
*	Add proof-nesting-depth, new implementation of span amalgamation in ↵	David Aspinall	2002-06-11
\| \| \| \|	proof-done-advancing.
*	Robustness fixes/bug notes	David Aspinall	2002-06-08
\|
*	Dont set type property for proof elements (experiment). Tweak name ↵	David Aspinall	2002-03-21
\| \| \| \|	determination/reporting. Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings
*	Simplify fix for repeated comments (commentre includes whitespace).	David Aspinall	2002-01-31
\|
*	Fix problem noticed with Isar and repeated comments.	David Aspinall	2002-01-31
\|
*	Also bury trace buffer	David Aspinall	2002-01-16
\|
*	Change to font-lock support routines.	David Aspinall	2001-12-11
\|
*	Fix problem with C-x C-v by copying buffer-file-name. Add children property ↵	David Aspinall	2001-09-05
\| \| \| \|	to control spans.
*	Nested proof spans are duplicable	David Aspinall	2001-09-04
\|
*	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.
*	Formatting	David Aspinall	2001-09-03
\|
*	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.
*	Clean up of proof-depends	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;
*	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
*	Change of proof span type back to goalsave fix	David Aspinall	2001-08-28
\|
*	Trim visibility implementation:	David Aspinall	2001-08-17
\| \| \| \| \|	- remove visibility specs and script portion records during undo - clear visibility specs on restart
*	Generate intermediate proof span for contents of proof; other becomes ↵	David Aspinall	2001-08-16
\| \| \| \|	'goalsave again. Add idiom property.
*	Use proof-looking-at-syntactic-context function from proof-syntax, as ↵	David Aspinall	2001-08-10
\| \| \| \|	suggested by Markus
*	Change buffer-syntactic-context -> proof-buffer-syntactic-context	David Aspinall	2001-08-10
\|
*	Emacs fix (extent->span). Copyright update.	David Aspinall	2001-05-03
\|
*	fixed format strings in message, error, etc.	Makarius Wenzel	2001-01-11
\|
*	Removed accidently committed debugging code	David Aspinall	2000-12-22
\|