aboutsummaryrefslogtreecommitdiff
path: root/lego.el
AgeCommit message (Expand)Author
1998-09-03Renamed for new subdirectory structureDavid Aspinall
1998-09-03Removed dead codeDavid Aspinall
1998-08-14improved help submenu for LEGOThomas Kleymann
1998-08-07o removed log entryThomas Kleymann
1998-07-27Supports official LEGO release 1.3Thomas Kleymann
1998-06-10Added lego-init-syntax-table as function to initialize syntax entriesHealfdene Goguen
1998-06-03Added '?'s before single characters in define-keys for emacs19, atHealfdene Goguen
1998-06-02Generalized proof-retract-target, now parameterized byHealfdene Goguen
1998-05-29o outsourced indentation to proof-indentThomas Kleymann
1998-05-23improved support for InfoThomas Kleymann
1998-05-16implementation of `lego-shell-adjust-line-width' can now be called asThomas Kleymann
1998-05-15Changed variable names [s]ext to span.Healfdene Goguen
1998-05-12Added hook `proof-shell-insert-hook', which is initalized toHealfdene Goguen
1998-05-08Made separated indentation more elegant.Healfdene Goguen
1998-05-08Merged indentation code for LEGO and Coq into proof.el.Healfdene Goguen
1998-05-06Changed lego-undoable-commands-regexp to have "andI" and "andE"Healfdene Goguen
1998-05-06Added lego-info-dir so that location of script-management.info can beHealfdene Goguen
1998-05-05Added lego-goal-command-p to fix Coq's problem with "Definition".Healfdene Goguen
1998-04-27removed explicit reference to a binary in ctm's home directoryThomas Kleymann
1998-03-25added support for etags at generic proof levelThomas Kleymann
1998-02-10added Dnf to lego-undoable-commands-regexpThomas Kleymann
1998-01-16Commented the code of proof.el and lego.el a bit. Made a minor changeDilip Sequiera
1998-01-15Updated method of defining proof-shell-cd to be consistent with otherHealfdene Goguen
1998-01-05fixed a bug in the indenting functionsThomas Kleymann
1997-11-26o simplified code:Thomas Kleymann
1997-11-24Added proof-execute-minibuffer-cmd and scripting minor mode.Dilip Sequiera
1997-11-20Added lego-global-p as always false, but for consistency with Coq mode.Healfdene Goguen
1997-11-18Added indentation for lego-mode.Dilip Sequiera
1997-11-17Added some magic commands: proof-frob-locked-end, proof-try-command,Dilip Sequiera
1997-11-06Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which isHealfdene Goguen
1997-10-24New indentation for lego-count-undos (smile)Healfdene Goguen
1997-10-16o merged script management (1.20.2.11) on the main branchThomas Kleymann
1997-10-13lego-count-undos is now aware that comments are treated separatelyThomas Kleymann
1997-10-08*** empty log message ***Healfdene Goguen
1997-08-25minor change in font-lock patternThomas Kleymann
1996-12-12removed font-lock support for Error messages; this is now supported inThomas Kleymann
1996-12-09Speeded up proof-by-pointing thingsDilip Sequiera
1996-12-05added font-lock properties for pbp-lego-modeThomas Kleymann
1996-12-03minor extensions of regular expressionsThomas Kleymann
1996-12-03Minor fix for performance reasons.Dilip Sequiera
1996-12-03A few small fixes to deal with performance problems.Dilip Sequiera
1996-11-29o added logical macros as keywordsThomas Kleymann
1996-11-22*** empty log message ***Thomas Kleymann
1996-11-21*** empty log message ***Thomas Kleymann
1996-11-17Cleaned ext.el up a bit in terms of its namespace and the management ofDilip Sequiera
1996-11-13minor changes regarding regular expressionsThomas Kleymann
1996-11-13Fixed parenthesis matching to deal with commentsDilip Sequiera
1996-11-13Yves Bertot's proof by pointingThomas Kleymann
1996-11-12improved lego-outline-regexpThomas Kleymann
1996-11-10fix for incorrect lego-outline-regexpThomas Kleymann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 21:49:23 +0000