| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 1998-05-06 | Simpler procedure for compiling emacs lisp. | Healfdene Goguen | |
| Added coq-info-dir so that script-management.info can be hard-coded. | |||
| 1998-05-05 | Coq now restarts if going back to beginning of proof. | Healfdene Goguen | |
| 1998-05-05 | Updated to include changes for emacs19. | Healfdene Goguen | |
| Also includes some changes for "Definition" problem in Coq, where Definition couldn't be used for proof scripts. Finally, modified proof-dependencies-xemacs code to fix problem that undoing to (point-min) meant you couldn't type at first character. | |||
| 1998-05-05 | Simple white-space changes. | Healfdene Goguen | |
| 1998-05-05 | Removed because its functionality is subsumed by the xemacs and | Healfdene Goguen | |
| emacs19 files. | |||
| 1998-05-05 | Dependencies of proof mode for xemacs | Healfdene Goguen | |
| There may be one or two areas that can be unified with emacs19 dependencies. | |||
| 1998-05-05 | Dependencies of proof mode for emacs19 | Healfdene Goguen | |
| Still in progress! | |||
| 1998-05-05 | Added lego-goal-command-p to fix Coq's problem with "Definition". | Healfdene Goguen | |
| Removed lego-killref from menu. | |||
| 1998-05-05 | Made updates to fix problem with Definition, which couldn't be | Healfdene Goguen | |
| used with proof scripts. Removed some useless declarations. Removed Abort from menu. Now Reset's if user undoes to beginning of proof. Added command to increase undo limit for Coq, and set default to 100. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |