6 |
6 |
7 ### |
7 ### |
8 ### ML compiler settings (ESSENTIAL!) |
8 ### ML compiler settings (ESSENTIAL!) |
9 ### |
9 ### |
10 |
10 |
11 ## Uncomment and adapt one of the sections below. |
|
12 |
|
13 # Note that ML_HOME specifies the location of the actual compiler |
11 # Note that ML_HOME specifies the location of the actual compiler |
14 # binaries. Do not invent new ML system names unless you know what |
12 # binaries. Do not invent new ML system names unless you know what |
15 # you are doing. |
13 # you are doing. Only one of the sections below should be activated. |
16 |
14 |
17 # Poly/ML 3.x or later |
15 # Poly/ML 3.x and 4.0 |
18 POLYML_HOME=$(choosefrom \ |
16 POLYML_HOME=$(choosefrom \ |
|
17 "$ISABELLE_HOME/contrib/polyml-4.0" \ |
|
18 "$ISABELLE_HOME/contrib/polyml-3.x" \ |
19 "$ISABELLE_HOME/contrib/polyml" \ |
19 "$ISABELLE_HOME/contrib/polyml" \ |
20 "$ISABELLE_HOME/../polyml") |
20 "$ISABELLE_HOME/../polyml-4.0" \ |
|
21 "$ISABELLE_HOME/../polyml-3.x" \ |
|
22 "$ISABELLE_HOME/../polyml" \ |
|
23 "/usr/share/polyml-4.0" \ |
|
24 "/usr/share/polyml-3.x" \ |
|
25 "/usr/share/polyml") |
|
26 ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null || echo polyml) |
21 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) |
27 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) |
22 ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null) |
|
23 ML_HOME=$POLYML_HOME/$ML_PLATFORM |
28 ML_HOME=$POLYML_HOME/$ML_PLATFORM |
24 ML_OPTIONS="-h 30000" |
29 ML_OPTIONS="-h 30000" |
25 |
30 |
26 # Standard ML of New Jersey 110 or later |
31 # Standard ML of New Jersey 110 or later |
27 #ML_SYSTEM=smlnj-110 |
32 #ML_SYSTEM=smlnj-110 |
149 "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
154 "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
150 "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
155 "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
151 "$ISABELLE_INTERFACE") |
156 "$ISABELLE_INTERFACE") |
152 PROOFGENERAL_OPTIONS="" |
157 PROOFGENERAL_OPTIONS="" |
153 |
158 |
154 # X-Symbol mode |
159 # X-Symbol mode for Proof General |
155 XSYMBOL_HOME=$(choosefrom \ |
160 XSYMBOL_HOME=$(choosefrom \ |
156 "$ISABELLE_HOME/contrib/x-symbol" \ |
161 "$ISABELLE_HOME/contrib/x-symbol" \ |
157 "$ISABELLE_HOME/../x-symbol" \ |
162 "$ISABELLE_HOME/../x-symbol" \ |
158 "") |
163 "") |
159 |
164 |