aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-script.el
Commit message (Expand)AuthorAge
* 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
* CommentsGravatar David Aspinall2000-09-20
* Get rid of proof-segment-up-to-old.Gravatar David Aspinall2000-09-18
* added proof-retract-current-goalGravatar Christophe Raffalli2000-09-15
* added proper call to proof-remove-comment before matching with proof-xxx-with...Gravatar Christophe Raffalli2000-09-15
* Remove FIXME.Gravatar David Aspinall2000-09-14
* Remove ambitious promise to implement proper generic-find-and-forget.Gravatar David Aspinall2000-09-13
* Remove shell important setting from script ones.Gravatar David Aspinall2000-09-12
* Added proof-shell-annotated-prompt-regexp to important settings, removed safe...Gravatar David Aspinall2000-09-11
* Fix obscure problem with proof-segment-upto-cmdstart with buggy input.Gravatar David Aspinall2000-09-08
* Added Fiona's changes, cleaned up a little bitGravatar David Aspinall2000-08-14
* handle comment inside a command (patch by da);Gravatar Makarius Wenzel2000-08-03
* changes to add theorem dependencies recording in spansGravatar David Aspinall2000-07-19
* Fix mark buffer atomic problem (caused multiple file oddity with Isar), for n...Gravatar David Aspinall2000-06-26
* proof-script-find-next-entity: support list of match items;Gravatar Makarius Wenzel2000-06-16
* CommentGravatar David Aspinall2000-06-09
* Added special hack for Isar to include proof-terminal-char in sent string.Gravatar David Aspinall2000-06-06
* proof-segment-up-to-cmdstart/end: use proof-re-search, proof-looking-at!Gravatar Makarius Wenzel2000-06-04
* proof-segment-up-to-cmdstart: exclude leading blanks from command string;Gravatar Makarius Wenzel2000-06-04
* improved proof-segment-up-to-cmdstart: handle overlap of commandGravatar Makarius Wenzel2000-06-03
* Use proof-running-on-XEmacs variable. Don't set proof-segment-up-to alias if...Gravatar David Aspinall2000-06-01
* New parsing functions proof-segment-up-to-cmd{start,end}Gravatar David Aspinall2000-06-01
* Fixes for completion support.Gravatar David Aspinall2000-05-31
* Hairy parsing for Isar. Not finished (or working) yet.Gravatar David Aspinall2000-05-30
* Arg for proof-minibuffer-cmd: compact whitespace in region.Gravatar David Aspinall2000-05-30
* Fixed typo causing bug. Generic parsing updated (still wip)Gravatar David Aspinall2000-05-30
* Added doc of new prefix arg feature for proof-minibuffer-cmdGravatar David Aspinall2000-05-30
* Added prefix arg to proof-minibuffer-cmd to insert current region.Gravatar David Aspinall2000-05-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 15:34:35 +0000