| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2001-09-03 | Formatting | David Aspinall | |
| 2001-08-31 | Move theorem dependency code into proof-depends.el. | David Aspinall | |
| Added 'controlspan property to proof body spans: action will be controlled from the control span. (The 'goalsave is the parent). Replace 'highlight face with 'proof-mouse-highlight-face throughout. | |||
| 2001-08-31 | Clean up of proof-depends | David Aspinall | |
| 2001-08-30 | pg-add-proof-element: removed accidential (?) dynamic scoping on | Makarius Wenzel | |
| proofbodyspan; handle proof-script-integral-proofs; | |||
| 2001-08-30 | fixes for FSF Emacs for searching for goal span (don't call goal-command-p ↵ | David Aspinall | |
| on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated | |||
| 2001-08-28 | Change of proof span type back to goalsave fix | David Aspinall | |
| 2001-08-17 | Trim visibility implementation: | David Aspinall | |
| - remove visibility specs and script portion records during undo - clear visibility specs on restart | |||
| 2001-08-16 | Generate intermediate proof span for contents of proof; other becomes ↵ | David Aspinall | |
| 'goalsave again. Add idiom property. | |||
| 2001-08-10 | Use proof-looking-at-syntactic-context function from proof-syntax, as ↵ | David Aspinall | |
| suggested by Markus | |||
| 2001-08-10 | Change buffer-syntactic-context -> proof-buffer-syntactic-context | David Aspinall | |
| 2001-05-03 | Emacs fix (extent->span). Copyright update. | David Aspinall | |
| 2001-01-11 | fixed format strings in message, error, etc. | Makarius Wenzel | |
| 2000-12-22 | Removed accidently committed debugging code | David Aspinall | |
| 2000-12-22 | *** empty log message *** | Christophe Raffalli | |
| 2000-12-20 | Improvements to span handling | David Aspinall | |
| 2000-12-14 | Remove some user-level functions to pg-user. | David Aspinall | |
| Fix bug in proof-goto-end-of-locked. | |||
| 2000-12-06 | fixed format strings for (message ...); | Makarius Wenzel | |
| 2000-10-30 | *** empty log message *** | Christophe Raffalli | |
| 2000-10-27 | *** empty log message *** | Christophe Raffalli | |
| 2000-09-29 | Parse comments also in proof-script-generic-parse-sexp | David Aspinall | |
| 2000-09-28 | Fix comment. | David Aspinall | |
| 2000-09-28 | Bug fix in proof-goto-end-of-locked. Comments in new parsing functions. ↵ | David Aspinall | |
| Tweaks to proof-script-generic-parse-cmdstart. Combine fly-past and coelesce comment options. Use proof-string-match-safe in generic-goal-command-p, to avoid error in Twelf. | |||
| 2000-09-27 | Added yet another new parsing mechanism, bit more rational this time. | David Aspinall | |
| 2000-09-23 | Remove require on proof-depends | David Aspinall | |
| Make toolbar commands work from non-scripting buffers Add save file dialogue to proof-register-possibly-new-processed-file | |||
| 2000-09-20 | Comments | David Aspinall | |
| 2000-09-18 | Get rid of proof-segment-up-to-old. | David Aspinall | |
| 2000-09-15 | added proof-retract-current-goal | Christophe Raffalli | |
| 2000-09-15 | added proper call to proof-remove-comment before matching with ↵ | Christophe Raffalli | |
| proof-xxx-with-hole-regexp | |||
| 2000-09-14 | Remove FIXME. | David Aspinall | |
| 2000-09-13 | Remove ambitious promise to implement proper generic-find-and-forget. | David Aspinall | |
| 2000-09-12 | Remove shell important setting from script ones. | David Aspinall | |
| 2000-09-11 | Added proof-shell-annotated-prompt-regexp to important settings, removed ↵ | David Aspinall | |
| safe default of empty string (now will have error msgs from filter) | |||
| 2000-09-08 | Fix obscure problem with proof-segment-upto-cmdstart with buggy input. | David Aspinall | |
| 2000-08-14 | Added Fiona's changes, cleaned up a little bit | David Aspinall | |
| 2000-08-03 | handle comment inside a command (patch by da); | Makarius Wenzel | |
| 2000-07-19 | changes to add theorem dependencies recording in spans | David Aspinall | |
| 2000-06-26 | Fix mark buffer atomic problem (caused multiple file oddity with Isar), for ↵ | David Aspinall | |
| new parsing functions. | |||
| 2000-06-16 | proof-script-find-next-entity: support list of match items; | Makarius Wenzel | |
| replaced spurious re-search-forward by proof-re-search-forward; proof-script-important-settings: commented out proof-goal-with-hole-regexp, proof-save-with-hole-regexp; | |||
| 2000-06-09 | Comment | David Aspinall | |
| 2000-06-06 | Added special hack for Isar to include proof-terminal-char in sent string. | David Aspinall | |
| 2000-06-04 | proof-segment-up-to-cmdstart/end: use proof-re-search, proof-looking-at! | Makarius Wenzel | |
| 2000-06-04 | proof-segment-up-to-cmdstart: exclude leading blanks from command string; | Makarius Wenzel | |
| 2000-06-03 | improved proof-segment-up-to-cmdstart: handle overlap of command | Makarius Wenzel | |
| prefix and comment/string (e.g. { vs {* in Isar); | |||
| 2000-06-01 | Use proof-running-on-XEmacs variable. Don't set proof-segment-up-to alias ↵ | David Aspinall | |
| if already set. | |||
| 2000-06-01 | New parsing functions proof-segment-up-to-cmd{start,end} | David Aspinall | |
| Select new parsing function according to config variables Use proof-comment-{start,end}-regexp, and set default values in proof-config-done-related, from proof-comment-{start,end} New proof-script-complete which uses proof-case-fold-search | |||
| 2000-05-31 | Fixes for completion support. | David Aspinall | |
| 2000-05-30 | Hairy parsing for Isar. Not finished (or working) yet. | David Aspinall | |
| 2000-05-30 | Arg for proof-minibuffer-cmd: compact whitespace in region. | David Aspinall | |
| 2000-05-30 | Fixed typo causing bug. Generic parsing updated (still wip) | David Aspinall | |
| 2000-05-30 | Added doc of new prefix arg feature for proof-minibuffer-cmd | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |