aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Expand)Author
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
2000-08-14Added Fiona's changes, cleaned up a little bitDavid Aspinall
2000-08-03handle comment inside a command (patch by da);Makarius Wenzel
2000-07-19changes to add theorem dependencies recording in spansDavid Aspinall
2000-06-26Fix mark buffer atomic problem (caused multiple file oddity with Isar), for n...David Aspinall
2000-06-16proof-script-find-next-entity: support list of match items;Makarius Wenzel
2000-06-09CommentDavid Aspinall
2000-06-06Added special hack for Isar to include proof-terminal-char in sent string.David Aspinall
2000-06-04proof-segment-up-to-cmdstart/end: use proof-re-search, proof-looking-at!Makarius Wenzel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:58:30 +0000