aboutsummaryrefslogtreecommitdiff
path: root/proof.el
AgeCommit message (Expand)Author
1998-09-03Renamed for new subdirectory structureDavid Aspinall
1998-09-03Added some documentation. Fixed a bug: indent-line-function needsDavid Aspinall
1998-08-26proof is now able to inherit append-element from tl-listThomas Kleymann
1998-08-25Added further documentation.Thomas Kleymann
1998-08-21Added comments. Made wakeup-char an option.David Aspinall
1998-08-14improved help submenu for LEGOThomas Kleymann
1998-08-11Renamed <file>-fontlock to <file>-syntaxDavid Aspinall
1998-08-07o removed log entryThomas Kleymann
1998-06-11Moved proof-mode-hooks from proof-shell-config-done toHealfdene Goguen
1998-06-10In proof-init-segmentation, only create proof-queue-span andHealfdene Goguen
1998-06-10Added proof-unprocessed-begin as general function to find beginning ofHealfdene 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-03Added (require 'cl) for emacs19.Healfdene Goguen
1998-06-03Added proof-goto-end-of-locked-interactive as oldHealfdene Goguen
1998-06-02Generalized proof-retract-target, now parameterized byHealfdene 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-26Removed commented code in proof-dont-show-annotationsHealfdene Goguen
1998-05-23improved support for InfoThomas Kleymann
1998-05-22fixed a bug in proof-frob-locked-endThomas Kleymann
1998-05-21Made proof-locked-span and proof-queue-span buffer-local.Healfdene Goguen
1998-05-19Changed proof-indent-line code so that it doesn't modify buffer ifHealfdene Goguen
1998-05-15Dependencies on versions of emacs have been moved to span-extent.elHealfdene Goguen
1998-05-12Added hook `proof-shell-insert-hook', to replace `proof-shell-config'.Healfdene 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-06Fixed bug with inserting commands and proof-shell-config.Healfdene Goguen
1998-05-06Removed proof-dependencies-emacs19 for the moment, since not having itHealfdene Goguen
1998-05-05Updated to include changes for emacs19.Healfdene Goguen
1998-03-25added support for etags at generic proof levelThomas Kleymann
1998-03-24*** empty log message ***Thomas 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-12o added support for remote proof processesThomas Kleymann
1998-01-05improved fume supportThomas Kleymann
1997-12-18o introduced proof-shell-handle-error-hook and bount it by default toThomas Kleymann
1997-11-26o The response buffer focusses on the first goalThomas Kleymann
1997-11-24Added proof-execute-minibuffer-cmd and scripting minor mode.Dilip Sequiera
1997-11-20Added proof-global-p to test whether a 'vanilla should be lifted aboveHealfdene Goguen
1997-11-17Added some magic commands: proof-frob-locked-end, proof-try-command,Dilip Sequiera
1997-11-13Includes commented code for Coq version of extent protocolHealfdene Goguen
1997-11-10Started modifications for emacs19 port.Dilip Sequiera
1997-11-10Put in a workaround for a strange bug in comint which was finding a bunchDilip Sequiera
1997-11-06Parameterize by proof-goal-hyp-fn in pbp-make-top-extent, to handleHealfdene Goguen
1997-10-31o implented proof-find-next-terminator available via C-c C-eThomas Kleymann
1997-10-30Updates for coq, including:Healfdene Goguen
1997-10-24Updated comment about extent typesHealfdene Goguen
1997-10-22Updated proof-segment-up-to to take ""'s into accountHealfdene Goguen
1997-10-17proof-active-terminator inside comment case fixed. Also maybe theDilip Sequiera
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 18:28:24 +0000