| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2002-06-08 | Robustness fixes/bug notes | David Aspinall | |
| 2002-03-21 | Dont set type property for proof elements (experiment). Tweak name ↵ | David Aspinall | |
| determination/reporting. Provide generic implementation of find-and-forget. Dont warn about some unnecessary settings | |||
| 2002-01-31 | Simplify fix for repeated comments (commentre includes whitespace). | David Aspinall | |
| 2002-01-31 | Fix problem noticed with Isar and repeated comments. | David Aspinall | |
| 2002-01-16 | Also bury trace buffer | David Aspinall | |
| 2001-12-11 | Change to font-lock support routines. | David Aspinall | |
| 2001-09-05 | Fix problem with C-x C-v by copying buffer-file-name. Add children property ↵ | David Aspinall | |
| to control spans. | |||
| 2001-09-04 | Nested proof spans are duplicable | David Aspinall | |
| 2001-09-03 | Show/hide all proofs: add redisplay for FSF | David Aspinall | |
| Use new functions pg-set-span-helphighlights and pg-span-name to set help echo, balloon help, mouse highlight, and context menu. | |||
| 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 | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |