aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
Commit message (Expand)AuthorAge
* Variable name change proof-comment-{start,end}-regexp -> proof-script-comment...Gravatar David Aspinall2002-07-19
* Add note about proof-generic-state-preserving-pGravatar David Aspinall2002-07-17
* CleanupsGravatar David Aspinall2002-07-17
* condition-case -> ignore-errors, comment.Gravatar David Aspinall2002-07-12
* proof-restart: also remove idiom internal spans.Gravatar David Aspinall2002-07-01
* Fix error catching in proof-deactivate-scripting-auto.Gravatar David Aspinall2002-06-30
* When killing process or scripting buffer, register file if it is complete, ra...Gravatar David Aspinall2002-06-30
* use-old-parser setting replaces use-new-parser setting [WARNING: big change]Gravatar David Aspinall2002-06-24
* GPLGravatar David Aspinall2002-06-21
* Remove lift-global function.Gravatar David Aspinall2002-06-18
* Remove global testing and lift-global function; rename proof-nested-goals -> ...Gravatar David Aspinall2002-06-18
* A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ...Gravatar David Aspinall2002-06-13
* Adjust proof-nesting depth, add FIXME notes since not right yetGravatar David Aspinall2002-06-12
* Add nestedundos setting to span, and proof-nested-undo-regexp settingGravatar David Aspinall2002-06-12
* Only match saves for prover that supports nested proofs (restores old behavio...Gravatar David Aspinall2002-06-11
* Improved proof-nesting-depth (not finished yet)Gravatar David Aspinall2002-06-11
* Add proof-nesting-depth, new implementation of span amalgamation in proof-don...Gravatar David Aspinall2002-06-11
* Robustness fixes/bug notesGravatar David Aspinall2002-06-08
* Dont set type property for proof elements (experiment). Tweak name determina...Gravatar David Aspinall2002-03-21
* Simplify fix for repeated comments (commentre includes whitespace).Gravatar David Aspinall2002-01-31
* Fix problem noticed with Isar and repeated comments.Gravatar David Aspinall2002-01-31
* Also bury trace bufferGravatar David Aspinall2002-01-16
* Change to font-lock support routines.Gravatar David Aspinall2001-12-11
* Fix problem with C-x C-v by copying buffer-file-name. Add children property t...Gravatar David Aspinall2001-09-05
* Nested proof spans are duplicableGravatar David Aspinall2001-09-04
* Show/hide all proofs: add redisplay for FSFGravatar David Aspinall2001-09-03
* FormattingGravatar David Aspinall2001-09-03
* Move theorem dependency code into proof-depends.el.Gravatar David Aspinall2001-08-31
* Clean up of proof-dependsGravatar David Aspinall2001-08-31
* pg-add-proof-element: removed accidential (?) dynamic scoping onGravatar Makarius Wenzel2001-08-30
* fixes for FSF Emacs for searching for goal span (don't call goal-command-p on...Gravatar David Aspinall2001-08-30
* Change of proof span type back to goalsave fixGravatar David Aspinall2001-08-28
* Trim visibility implementation:Gravatar David Aspinall2001-08-17
* Generate intermediate proof span for contents of proof; other becomes 'goalsa...Gravatar David Aspinall2001-08-16
* Use proof-looking-at-syntactic-context function from proof-syntax, as suggest...Gravatar David Aspinall2001-08-10
* Change buffer-syntactic-context -> proof-buffer-syntactic-contextGravatar David Aspinall2001-08-10
* Emacs fix (extent->span). Copyright update.Gravatar David Aspinall2001-05-03
* fixed format strings in message, error, etc.Gravatar Makarius Wenzel2001-01-11
* Removed accidently committed debugging codeGravatar David Aspinall2000-12-22
* *** empty log message ***Gravatar Christophe Raffalli2000-12-22
* Improvements to span handlingGravatar David Aspinall2000-12-20
* Remove some user-level functions to pg-user.Gravatar David Aspinall2000-12-14
* fixed format strings for (message ...);Gravatar Makarius Wenzel2000-12-06
* *** empty log message ***Gravatar Christophe Raffalli2000-10-30
* *** empty log message ***Gravatar Christophe Raffalli2000-10-27
* Parse comments also in proof-script-generic-parse-sexpGravatar David Aspinall2000-09-29
* Fix comment.Gravatar David Aspinall2000-09-28
* Bug fix in proof-goto-end-of-locked. Comments in new parsing functions. Twe...Gravatar David Aspinall2000-09-28
* Added yet another new parsing mechanism, bit more rational this time.Gravatar David Aspinall2000-09-27
* Remove require on proof-dependsGravatar David Aspinall2000-09-23