aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
1998-06-11Added "Scheme" as definition keyword.Healfdene Goguen
1998-06-10Wrote generic span functions for making spans read-only or read-write.Healfdene Goguen
1998-06-10Wrote generic span functions for making spans read-only or read-write.Healfdene Goguen
1998-06-10In proof-init-segmentation, only create proof-queue-span andHealfdene Goguen
1998-06-10Compare span-end first rather than span-start in span-lt, becauseHealfdene Goguen
1998-06-10Added proof-unprocessed-begin as general function to find beginning ofHealfdene Goguen
1998-06-10Changed "\\s " to "\\s-" in proof-id as whitespace pattern.Healfdene Goguen
1998-06-10Added lego-init-syntax-table as function to initialize syntax entriesHealfdene Goguen
1998-06-10Added coq-init-syntax-table as function to initialize syntax entriesHealfdene Goguen
1998-06-10Added "Mutual Inductive" as definition keyword.Healfdene Goguen
1998-06-09o fixed bug in setting proof-queue-face on a colour terminal for GNUThomas Kleymann
1998-06-03Added '?'s before single characters in define-keys for emacs19, atHealfdene Goguen
1998-06-03Changed Compute from command to tactic.Healfdene Goguen
1998-06-03Changed last-span to before-list.Healfdene Goguen
1998-06-03Added (require 'cl) for emacs19.Healfdene Goguen
1998-06-03Added proof-goto-end-of-locked-interactive as oldHealfdene Goguen
1998-06-03Changed expression (>= 0 x) to its equivalent (eq x 0)Healfdene Goguen
1998-06-03Added definition of proof-commands-regexp for coqHealfdene Goguen
1998-06-02Structured review now done.Healfdene Goguen
1998-06-02Corrected comment about this being for emacs19.Healfdene Goguen
1998-06-02Corrected comment about this being for xemacs.Healfdene Goguen
1998-06-02Added comment about C-c ' that it will switch to the scripting buffer.Healfdene Goguen
1998-06-02Generalized proof-retract-target, now parameterized byHealfdene Goguen
1998-06-02Generalized proof-retract-target, now parameterized byHealfdene Goguen
1998-06-02Minor modifications to commentsHealfdene Goguen
1998-05-29fixed a bug in `proof-goto-end-of-locked-if-pos-not-visible-in-window'Thomas Kleymann
1998-05-29o outsourced indentation to proof-indentThomas Kleymann
1998-05-26Necessary changes for emacs19 versionHealfdene Goguen
1998-05-26Removed commented code in proof-dont-show-annotationsHealfdene Goguen
1998-05-23improved support for InfoThomas Kleymann
1998-05-22Correct path for coq-prog-name and coq-tags.Healfdene Goguen
1998-05-22fixed a bug in proof-frob-locked-endThomas Kleymann
1998-05-22included "Invert" in `lego-keywords'Thomas Kleymann
1998-05-21Made proof-locked-span and proof-queue-span buffer-local.Healfdene Goguen
1998-05-21Removed uninitialized os variable in spans-at-region.Healfdene Goguen
1998-05-21Changing buffers now works.Healfdene Goguen
1998-05-21Fixed lifting globals.Healfdene Goguen
1998-05-21Initialize 'before pointer in add-span-aux when last-span is nil.Healfdene Goguen
1998-05-19Removed indentation problem.Healfdene Goguen
1998-05-19Added header and log message.Healfdene Goguen
1998-05-19Added header and log message.Healfdene Goguen
1998-05-19Changed proof-indent-line code so that it doesn't modify buffer ifHealfdene Goguen
1998-05-16*** empty log message ***Thomas Kleymann
1998-05-16implementation of `lego-shell-adjust-line-width' can now be called asThomas Kleymann
1998-05-15Added problem with indentation.Healfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-15Changed variable names [s]ext to span.Healfdene Goguen
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 15:46:41 +0000