| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-05-26 | Removed commented code in proof-dont-show-annotations | Healfdene Goguen | |
| proof-done-trying deletes the spans that were created | |||
| 1998-05-23 | improved support for Info | Thomas Kleymann | |
| o employed `Info-default-directory-list' rather than `Info-directory-list' so that code also works for Emacs 19.34 o setting of `Info-default-directory-list' now at proof level | |||
| 1998-05-22 | Correct path for coq-prog-name and coq-tags. | Healfdene Goguen | |
| 1998-05-22 | fixed a bug in proof-frob-locked-end | Thomas Kleymann | |
| 1998-05-22 | included "Invert" in `lego-keywords' | Thomas Kleymann | |
| 1998-05-21 | Made proof-locked-span and proof-queue-span buffer-local. | Healfdene Goguen | |
| Changed some if's without then-clauses to and's. Removed (proof-detach-segments) from (proof-steal-process) This is the bug that made changing buffers fail in emacs19: the segments had already been detached. Check if we're in proof buffer for proof-frob-locked-end. Force mode-line update for emacs19 in proof-active-terminator-minor-mode. | |||
| 1998-05-21 | Removed uninitialized os variable in spans-at-region. | Healfdene Goguen | |
| 1998-05-21 | Changing buffers now works. | Healfdene Goguen | |
| 1998-05-21 | Fixed lifting globals. | Healfdene Goguen | |
| Added problem of buffers and need for incremental adding of tactics in Coq. | |||
| 1998-05-21 | Initialize 'before pointer in add-span-aux when last-span is nil. | Healfdene Goguen | |
| Removed span-at-type. Fixed bug in span-at-before, where (span-start span) may be nil. Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end of buffer. | |||
| 1998-05-19 | Removed indentation problem. | Healfdene Goguen | |
| Added comments about current state of emacs19 port. | |||
| 1998-05-19 | Added header and log message. | Healfdene Goguen | |
| Fixed set-span-endpoints so it preserves invariant. Changed add-span and remove-span so that they update last-span correctly themselves, and don't take last-span as an argument. | |||
| 1998-05-19 | Added header and log message. | Healfdene Goguen | |
| 1998-05-19 | Changed proof-indent-line code so that it doesn't modify buffer if | Healfdene Goguen | |
| nothing is changed. Changed proof-indent-region code so that the endpoints of the region being indented change as indentation is done: it was infinite looping because the end could never be reached. | |||
| 1998-05-16 | *** empty log message *** | Thomas Kleymann | |
| 1998-05-16 | implementation of `lego-shell-adjust-line-width' can now be called as | Thomas Kleymann | |
| part of a hook. This change has been caused by replacing `proof-shell-config' with `proof-shell-insert-hook' | |||
| 1998-05-15 | Added problem with indentation. | Healfdene Goguen | |
| 1998-05-15 | Dependencies on versions of emacs have been moved to span-extent.el | Healfdene Goguen | |
| and span-overlay.el. This file was developed under xemacs, but runs for emacs19 as well. | |||
| 1998-05-15 | Dependencies on versions of emacs have been moved to span-extent.el | Healfdene Goguen | |
| and span-overlay.el. This file was developed for xemacs. | |||
| 1998-05-15 | Dependencies on versions of emacs have been moved to span-extent.el | Healfdene Goguen | |
| and span-overlay.el. Definitions of proof-queue-span and proof-locked-span now in proof.el. Changed variable names [s]ext to span. | |||
| 1998-05-15 | Dependencies on versions of emacs have been moved to span-extent.el | Healfdene Goguen | |
| and span-overlay.el. | |||
| 1998-05-15 | Changed variable names [s]ext to span. | Healfdene Goguen | |
| 1998-05-15 | Changed variable names [s]ext to span. | Healfdene Goguen | |
| Fixed coq-find-and-forget pattern for declarations and definitions following Pascal Brisset's suggestion. | |||
| 1998-05-15 | Added CoFixpoint and tactics. | Healfdene Goguen | |
| Changed indentation. | |||
| 1998-05-14 | Changes to indentation code: | Healfdene Goguen | |
| Changed "case" to "Case". Added "CoInductive". | |||
| 1998-05-14 | Updated install script after finding problems with Savi's setup. | Healfdene Goguen | |
| 1998-05-13 | revised in light of today's meeting with hhg | Thomas Kleymann | |
| 1998-05-12 | Added documentation for C-c C-s in Coq mode. | Healfdene Goguen | |
| Fixed problem with tabbing changing buffers. | |||
| 1998-05-12 | Added documentation for C-c C-s in Coq mode. | Healfdene Goguen | |
| 1998-05-12 | Added hook `proof-shell-insert-hook', to replace `proof-shell-config'. | Healfdene Goguen | |
| 1998-05-12 | Added hook `proof-shell-insert-hook', which is initalized to | Healfdene Goguen | |
| lego-shell-adjust-line-width. This replaces `lego-shell-config'. | |||
| 1998-05-12 | Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'. | Healfdene Goguen | |
| This initializes undo limit and changes directory to that associated with buffer. This is because Coq has a command line option to run with emacs mode. | |||
| 1998-05-08 | Made separated indentation more elegant: | Healfdene Goguen | |
| Made proof-assistant specific code into separate procedure, proof-parse-indent. Separated consideration of {}'s so it only happens for LEGO. | |||
| 1998-05-08 | Made separated indentation more elegant. | Healfdene Goguen | |
| Separated consideration of {}'s so it only happens for LEGO. | |||
| 1998-05-08 | Made separated indentation more elegant. | Healfdene Goguen | |
| Fixed bug with Inductive. Added CoInductive. | |||
| 1998-05-08 | Merged indentation code for LEGO and Coq into proof.el. | Healfdene Goguen | |
| 1998-05-08 | Updated todo list. | Healfdene Goguen | |
| 1998-05-08 | Merged indentation code for LEGO and Coq into proof.el. | Healfdene Goguen | |
| Fixed problem with active terminator mode: [proof-terminal-char] isn't the same as (vector proof-terminal-char). | |||
| 1998-05-08 | Merged indentation code for LEGO and Coq into proof.el. | Healfdene Goguen | |
| 1998-05-06 | Fixed bug with inserting commands and proof-shell-config. | Healfdene Goguen | |
| 1998-05-06 | Removed default instantiation of undo limit to 100. | Healfdene Goguen | |
| 1998-05-06 | Added comments about info file and default values in coq.el. | Healfdene Goguen | |
| 1998-05-06 | Removed proof-dependencies-emacs19 for the moment, since not having it | Healfdene Goguen | |
| introduces error messages. Put cd before init in proof-shell-config-done (this won't work for Coq). | |||
| 1998-05-06 | Fixed problem introduced by working on emacs19 in | Healfdene Goguen | |
| proof-zap-commas-region. | |||
| 1998-05-06 | Changed lego-undoable-commands-regexp to have "andI" and "andE" | Healfdene Goguen | |
| instead of "AndI" and "AndE". | |||
| 1998-05-06 | First checked-in version. | Healfdene Goguen | |
| 1998-05-06 | Basic description of script management, in texinfo format. | Healfdene Goguen | |
| 1998-05-06 | Basic description of script management, compiled for emacs info mode. | Healfdene Goguen | |
| 1998-05-06 | Added lego-info-dir so that location of script-management.info can be | Healfdene Goguen | |
| hard-coded. | |||
| 1998-05-06 | Added coq-info-dir so that script-management.info can be hard-coded. | Healfdene Goguen | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |