Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added proof-rsh-command to help complete documentation (was allocated | 1998-11-09 | |
| | | | | to tms but he said he wouldn't get around to it) | ||
* | Added proof-script-indent user option, to enable indentation code. | 1998-11-09 | |
| | | | | | | Disabled by default. May be activated by particular proof assistants if they feel confident about it. I don't. Made proof-indent be autoloaded as needed. Lets pray it won't be. | ||
* | Added proof-strict-read-only, probably a handy new user-option. | 1998-11-09 | |
| | | | | | | Side effect is that it's default value of nil for FSF Emacs avoids the font lock problem with span-read-only for FSF Emacs. XEmacs does not have the warning message implemented yet. | ||
* | Being pedantic about variables versus predicates, renamed prog-name-ask-p. | 1998-11-03 | |
| | |||
* | Customization group and type fixes | 1998-11-03 | |
| | |||
* | Improved docstrings | 1998-11-03 | |
| | |||
* | Promoted proof-window-dedicated to be a user option, and | 1998-11-03 | |
| | | | | renamed it [to reserve -p only for functions (predicates)]. | ||
* | fixed bug with font-lock face names | 1998-11-03 | |
| | |||
* | o added support for byte-compilation | 1998-11-01 | |
| | | | | | | | o removed hhg tags in todo o fixed font-lock for FSF Emacs 20.2 o ensured that goals buffer is updated for longer queues o fixed a bug in proof-universal-keys-only-mode | ||
* | implemented new buffer model. The goals buffer is now exclusively | 1998-10-30 | |
| | | | | reserved for goals. | ||
* | Clarifying comment about obscure variable added | 1998-10-29 | |
| | |||
* | More hacks to variable names for customize (sorry) | 1998-10-29 | |
| | |||
* | Added prefixes in custom defgroups. | 1998-10-29 | |
| | |||
* | Added customize group for Proof General faces and fixed other | 1998-10-28 | |
| | | | | groups in proof-config. | ||
* | Continuing mods for cleaner byte compile | 1998-10-27 | |
| | |||
* | Made handling of multiple files more robust. On changing script | 1998-10-27 | |
| | | | | | buffers, we invoke (save-some-buffers). Furthermore, we warn the user if modified buffers have been read in by the proof assistant. | ||
* | Fixed up proof-script.el for clean byte compile | 1998-10-27 | |
| | |||
* | typo | 1998-10-27 | |
| | |||
* | Moved pbp-goal-command and pbp-hyp-command to proof-config.Moved LEGO specifix. | 1998-10-27 | |
| | |||
* | Begun work on clean byte compilation / clarifying interfaces. | 1998-10-27 | |
| | |||
* | Fixed urgent message stuff. proof-shell-process-urgent-messages | 1998-10-27 | |
| | | | | now seems to correctly observe all messages which pass through. | ||
* | Added note about mode symbols | 1998-10-23 | |
| | |||
* | Added proof-mode-for-script setting. | 1998-10-23 | |
| | |||
* | Replaced remaining face defs with defface calls. | 1998-10-23 | |
| | | | | | Removed font-lock-<newface> with proof-<newface> so we know where things come from and won't break future font locks. | ||
* | Added deffaces to proof-config | 1998-10-22 | |
| | |||
* | Added todo for clean byte compile | 1998-10-22 | |
| | |||
* | Split proof.el into proof-config.el, proof-script.el, proof-shell.el | 1998-10-22 | |