diff options
| -rw-r--r-- | CHANGES | 18 | ||||
| -rw-r--r-- | INSTALL | 16 |
2 files changed, 28 insertions, 6 deletions
@@ -38,6 +38,21 @@ Also, for XEmacs, there are now (trivial) help messages in echo area describing the highlighted region under the mouse. +*** Experimental features and new user option + + There's a new user option `proof-experimental-features' which + is nil by default. If you set it to t, you will (maybe after + restarting Proof General) enable certain experimental features. + + In this release, the experimental features are: + + Context menu options to move spans up/down + Context menu dependency commands (Isabelle only, see below) + + To customize this from the menu: + + Proof General -> Customize -> User Options -> Experimental features + *** Proof General startup script welcomes user The "binary" (startup script) bin/proofgeneral now loads @@ -126,6 +141,9 @@ restart. (This behaviour will improve once better integrated with Isabelle). + NB this is classed as an experimental feature, so you must set + proof-experimental-features to enable it. + Not yet documented. Comments and suggestions welcome. @@ -105,12 +105,16 @@ Byte Compilation. ----------------- Compilation of the Emacs lisp files improves efficiency but can -sometimes cause compatibility problems. It is not supported in this -release. If you want to experiment nonetheless, you can compile Proof -General by typing 'make' in the directory where you installed it. -This will result in lots of warnings and error messages most of which -can be ignored. Check the Makefile sets EMACS to your Emacs -executable. +sometimes cause compatibility problems. It is not properly supported +in this release, because testing for these compatibility problems +takes too much time. If you want to experiment nonetheless, you can +compile Proof General by typing 'make' in the directory where you +installed it. This will result in lots of warnings and error messages +most of which can be ignored. Some files cannot be properly +byte-compiled at the moment because they contain settings which depend +on run-time; these will be deleted by the Makefile. Use 'make clean' +to remove all .elc files in case of problems. Check the Makefile sets +EMACS to your Emacs executable. Site-wide Installation |