added ProofGeneral settings;
authorwenzelm
Mon Dec 11 12:28:16 2006 +0100 (2006-12-11)
changeset 21764720b0add5206
parent 21763 12a2773e3608
child 21765 89275a3ed7be
added ProofGeneral settings;
Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
     1.1 --- a/Admin/Isabelle2005-polyml-5.0/README-polyml-5.0	Sun Dec 10 22:27:06 2006 +0100
     1.2 +++ b/Admin/Isabelle2005-polyml-5.0/README-polyml-5.0	Mon Dec 11 12:28:16 2006 +0100
     1.3 @@ -5,19 +5,30 @@
     1.4    Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
     1.5    Isabelle2005/lib/scripts/run-polyml-5.0
     1.6  
     1.7 -Moreover the Isabelle settings need to specify that version, by
     1.8 -including something like this in Isabelle2005/etc/settings or
     1.9 +The Isabelle settings need to specify that version, by including
    1.10 +something like this in Isabelle2005/etc/settings or
    1.11  ~/isabelle/etc/settings:
    1.12  
    1.13 -ML_PLATFORM=""
    1.14 -ML_HOME=/usr/local/bin
    1.15 -ML_SYSTEM=polyml-5.0
    1.16 -ML_OPTIONS="-H 500"
    1.17 +  ML_PLATFORM=""
    1.18 +  ML_HOME=/usr/local/bin
    1.19 +  ML_SYSTEM=polyml-5.0
    1.20 +  ML_OPTIONS="-H 500"
    1.21 +
    1.22 +Now logics can be compiled as usual, cf. the INSTALL instructions.
    1.23 +
    1.24  
    1.25 -Then logics can be compiled as usual, cf. the INSTALL instructions.
    1.26 +ProofGeneral needs to be adapted as well, by including the following
    1.27 +in Isabelle2005/etc/proofgeneral-settings.el or
    1.28 +~/isabelle/etc/proofgeneral-settings.el:
    1.29 +
    1.30 +  (custom-set-variables
    1.31 +   '(proof-shell-pre-interrupt-hook (lambda () t)))
    1.32 +
    1.33 +Otherwise ProofGeneral will regard polyml-5.0 as an old polyml-3.x and
    1.34 +activate strange workarounds for interrupt handling.
    1.35  
    1.36  
    1.37  	Makarius
    1.38 -	07-Dec-2006
    1.39 +	11-Dec-2006
    1.40  
    1.41  $Id$