From 4a9c2da087829312adff30e39d28faa101c795f0 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 3 Nov 1998 18:06:54 +0000 Subject: Updated and improved. --- BUGS | 12 +++++------- INSTALL | 19 ++++++++++++------- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/BUGS b/BUGS index 021fe130..d50971a1 100644 --- a/BUGS +++ b/BUGS @@ -6,19 +6,17 @@ $Id$ * Toolbar: retract button can give "BUG" error message "called from wrong buffer" when the process is inactive. -* Toolbar: not updated properly. See redisplay-frame attempt -in proof-shell-filter. Why does this behave strangely? - * Ordinary undo in script buffer can edit the "uneditable region" -in XEmacs. This doesn't happen in FSFmacs! Test case: +in XEmacs. This doesn't happen in FSFmacs. Test case: Insert some nonsense text after the locked region. Kill the line. Process to the next command. - Press C-x u, nonsense text appears in locked region! + Press C-x u, nonsense text appears in locked region. +Workaround: take care with undo in XEmacs. * Using C-g can leave script management in a mess. The code needs to have some regions protected from Emacs interrupts. -At the moment, don't type C-g while script management is -processing. If you do, use proof-restart-scripting. +Workaround: Don't type C-g while script management is processing. If +you do, use proof-restart-scripting. * You can't use more than one proof assistant at a time in the same Emacs session. Nasty things happen if proof-assistants enables diff --git a/INSTALL b/INSTALL index 80f34f50..08295248 100644 --- a/INSTALL +++ b/INSTALL @@ -4,13 +4,17 @@ Instructions for installing Proof General This file describes what to do to be able to run Proof General. Please let us know if you have any problems in trying to install it. -Unpack this distribution in some . Put this line in your -.emacs file: +Unpack this distribution somewhere. It will create a top-level +directory containing Proof General, called Proof-General-. +Put this line in your emacs file: - (load-file "/generic/proof-site.el") + (load-file "/generic/proof-site.el") -This will set the Emacs load path and add auto-loads for the -assistants below: +Where is replaced by the full path to the +top-level directory made when you unpacked the distribution. + +The command above will set the Emacs load path and add auto-loads for +the assistants below: .v Coq files .l LEGO files @@ -19,8 +23,9 @@ assistants below: When you load a file with one of these extensions, the corresponding Proof General mode will be entered. -In case of difficulty, please check the notes below and the file BUGS. -If this doesn't help, then contact us via the address below. +In case of difficulty, please check the documentation in doc/, the +notes below, and the file BUGS. If this doesn't help, then contact us +via the address below. Proof General maintainer School of Computer Science, -- cgit v1.2.3