Admin/Isabelle2005-polyml-5.0/README-polyml-5.0
author wenzelm
Thu Oct 04 14:42:11 2007 +0200 (2007-10-04)
changeset 24829 e1214fa781ca
parent 21764 720b0add5206
permissions -rw-r--r--
avoid gensym;
wenzelm@21688
     1
wenzelm@21688
     2
Using Isabelle2005 with Poly/ML 5.0 requires the following
wenzelm@21688
     3
compatibility wrappers:
wenzelm@21688
     4
wenzelm@21688
     5
  Isabelle2005/src/Pure/ML-Systems/polyml-5.0.ML
wenzelm@21688
     6
  Isabelle2005/lib/scripts/run-polyml-5.0
wenzelm@21688
     7
wenzelm@21764
     8
The Isabelle settings need to specify that version, by including
wenzelm@21764
     9
something like this in Isabelle2005/etc/settings or
wenzelm@21688
    10
~/isabelle/etc/settings:
wenzelm@21688
    11
wenzelm@21764
    12
  ML_PLATFORM=""
wenzelm@21764
    13
  ML_HOME=/usr/local/bin
wenzelm@21764
    14
  ML_SYSTEM=polyml-5.0
wenzelm@21764
    15
  ML_OPTIONS="-H 500"
wenzelm@21764
    16
wenzelm@21764
    17
Now logics can be compiled as usual, cf. the INSTALL instructions.
wenzelm@21764
    18
wenzelm@21688
    19
wenzelm@21764
    20
ProofGeneral needs to be adapted as well, by including the following
wenzelm@21764
    21
in Isabelle2005/etc/proofgeneral-settings.el or
wenzelm@21764
    22
~/isabelle/etc/proofgeneral-settings.el:
wenzelm@21764
    23
wenzelm@21764
    24
  (custom-set-variables
wenzelm@21764
    25
   '(proof-shell-pre-interrupt-hook (lambda () t)))
wenzelm@21764
    26
wenzelm@21764
    27
Otherwise ProofGeneral will regard polyml-5.0 as an old polyml-3.x and
wenzelm@21764
    28
activate strange workarounds for interrupt handling.
wenzelm@21688
    29
wenzelm@21688
    30
wenzelm@21688
    31
	Makarius
wenzelm@21764
    32
	11-Dec-2006
wenzelm@21688
    33
wenzelm@21688
    34
$Id$