aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
AgeCommit message (Expand)Author
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
2000-06-04proof-segment-up-to-cmdstart: exclude leading blanks from command string;Makarius Wenzel
2000-06-03improved proof-segment-up-to-cmdstart: handle overlap of commandMakarius Wenzel
2000-06-01Use proof-running-on-XEmacs variable. Don't set proof-segment-up-to alias if...David Aspinall
2000-06-01New parsing functions proof-segment-up-to-cmd{start,end}David Aspinall
2000-05-31Fixes for completion support.David Aspinall
2000-05-30Hairy parsing for Isar. Not finished (or working) yet.David Aspinall
2000-05-30Arg for proof-minibuffer-cmd: compact whitespace in region.David Aspinall
2000-05-30Fixed typo causing bug. Generic parsing updated (still wip)David Aspinall
2000-05-30Added doc of new prefix arg feature for proof-minibuffer-cmdDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:45:19 +0000