# HG changeset patch
# User wenzelm
# Date 1165836496 -3600
# Node ID 720b0add52067e67f4a1767da6c2d64adae519e3
# Parent  12a2773e3608c56e9b09a15d60a0fe9cc0abe614
added ProofGeneral settings;

diff -r 12a2773e3608 -r 720b0add5206 Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
--- a/Admin/Isabelle2005-polyml-5.0/README-polyml-5.0	Sun Dec 10 22:27:06 2006 +0100
+++ b/Admin/Isabelle2005-polyml-5.0/README-polyml-5.0	Mon Dec 11 12:28:16 2006 +0100
@@ -5,19 +5,30 @@
   Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
   Isabelle2005/lib/scripts/run-polyml-5.0
 
-Moreover the Isabelle settings need to specify that version, by
-including something like this in Isabelle2005/etc/settings or
+The Isabelle settings need to specify that version, by including
+something like this in Isabelle2005/etc/settings or
 ~/isabelle/etc/settings:
 
-ML_PLATFORM=""
-ML_HOME=/usr/local/bin
-ML_SYSTEM=polyml-5.0
-ML_OPTIONS="-H 500"
+  ML_PLATFORM=""
+  ML_HOME=/usr/local/bin
+  ML_SYSTEM=polyml-5.0
+  ML_OPTIONS="-H 500"
+
+Now logics can be compiled as usual, cf. the INSTALL instructions.
+
 
-Then logics can be compiled as usual, cf. the INSTALL instructions.
+ProofGeneral needs to be adapted as well, by including the following
+in Isabelle2005/etc/proofgeneral-settings.el or
+~/isabelle/etc/proofgeneral-settings.el:
+
+  (custom-set-variables
+   '(proof-shell-pre-interrupt-hook (lambda () t)))
+
+Otherwise ProofGeneral will regard polyml-5.0 as an old polyml-3.x and
+activate strange workarounds for interrupt handling.
 
 
 	Makarius
-	07-Dec-2006
+	11-Dec-2006
 
 $Id$