aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Expand)Author
2002-06-18Remove lift-global function.David Aspinall
2002-06-18Remove global testing and lift-global function; rename proof-nested-goals -> ...David Aspinall
2002-06-13A nil setting of proof-kill-goal-command forces use of proof-find-and-forget ...David Aspinall
2002-06-12Adjust proof-nesting depth, add FIXME notes since not right yetDavid Aspinall
2002-06-12Add nestedundos setting to span, and proof-nested-undo-regexp settingDavid Aspinall
2002-06-11Only match saves for prover that supports nested proofs (restores old behavio...David Aspinall
2002-06-11Improved proof-nesting-depth (not finished yet)David Aspinall
2002-06-11Add proof-nesting-depth, new implementation of span amalgamation in proof-don...David Aspinall
2002-06-08Robustness fixes/bug notesDavid Aspinall
2002-03-21Dont set type property for proof elements (experiment). Tweak name determina...David Aspinall
2002-01-31Simplify fix for repeated comments (commentre includes whitespace).David Aspinall
2002-01-31Fix problem noticed with Isar and repeated comments.David Aspinall
2002-01-16Also bury trace bufferDavid Aspinall
2001-12-11Change to font-lock support routines.David Aspinall
2001-09-05Fix problem with C-x C-v by copying buffer-file-name. Add children property t...David Aspinall
2001-09-04Nested proof spans are duplicableDavid Aspinall
2001-09-03Show/hide all proofs: add redisplay for FSFDavid Aspinall
2001-09-03FormattingDavid Aspinall
2001-08-31Move theorem dependency code into proof-depends.el.David Aspinall
2001-08-31Clean up of proof-dependsDavid Aspinall
2001-08-30pg-add-proof-element: removed accidential (?) dynamic scoping onMakarius Wenzel
2001-08-30fixes for FSF Emacs for searching for goal span (don't call goal-command-p on...David Aspinall
2001-08-28Change of proof span type back to goalsave fixDavid Aspinall
2001-08-17Trim visibility implementation:David Aspinall
2001-08-16Generate intermediate proof span for contents of proof; other becomes 'goalsa...David Aspinall
2001-08-10Use proof-looking-at-syntactic-context function from proof-syntax, as suggest...David Aspinall
2001-08-10Change buffer-syntactic-context -> proof-buffer-syntactic-contextDavid Aspinall
2001-05-03Emacs fix (extent->span). Copyright update.David Aspinall
2001-01-11fixed format strings in message, error, etc.Makarius Wenzel
2000-12-22Removed accidently committed debugging codeDavid Aspinall
2000-12-22*** empty log message ***Christophe Raffalli
2000-12-20Improvements to span handlingDavid Aspinall
2000-12-14Remove some user-level functions to pg-user.David Aspinall
2000-12-06fixed format strings for (message ...);Makarius Wenzel
2000-10-30*** empty log message ***Christophe Raffalli
2000-10-27*** empty log message ***Christophe Raffalli
2000-09-29Parse comments also in proof-script-generic-parse-sexpDavid Aspinall
2000-09-28Fix comment.David Aspinall
2000-09-28Bug fix in proof-goto-end-of-locked. Comments in new parsing functions. Twe...David Aspinall
2000-09-27Added yet another new parsing mechanism, bit more rational this time.David Aspinall
2000-09-23Remove require on proof-dependsDavid Aspinall
2000-09-20CommentsDavid Aspinall
2000-09-18Get rid of proof-segment-up-to-old.David Aspinall
2000-09-15added proof-retract-current-goalChristophe Raffalli
2000-09-15added proper call to proof-remove-comment before matching with proof-xxx-with...Christophe Raffalli
2000-09-14Remove FIXME.David Aspinall
2000-09-13Remove ambitious promise to implement proper generic-find-and-forget.David Aspinall
2000-09-12Remove shell important setting from script ones.David Aspinall
2000-09-11Added proof-shell-annotated-prompt-regexp to important settings, removed safe...David Aspinall
2000-09-08Fix obscure problem with proof-segment-upto-cmdstart with buggy input.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 17:16:43 +0000