21 "$ISABELLE_HOME/../polyml-3.x" \ |
21 "$ISABELLE_HOME/../polyml-3.x" \ |
22 "$ISABELLE_HOME/../polyml" \ |
22 "$ISABELLE_HOME/../polyml" \ |
23 "/usr/share/polyml-4.0" \ |
23 "/usr/share/polyml-4.0" \ |
24 "/usr/share/polyml-3.x" \ |
24 "/usr/share/polyml-3.x" \ |
25 "/usr/share/polyml") |
25 "/usr/share/polyml") |
26 ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null || echo polyml) |
26 ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml) |
27 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) |
27 ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null) |
28 ML_HOME=$POLYML_HOME/$ML_PLATFORM |
28 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
29 ML_OPTIONS="-h 30000" |
29 ML_OPTIONS="-h 30000" |
30 |
30 |
31 # Standard ML of New Jersey 110 or later |
31 # Standard ML of New Jersey 110 or later |
32 #ML_SYSTEM=smlnj-110 |
32 #ML_SYSTEM=smlnj-110 |
33 #ML_HOME=$ISABELLE_HOME/../smlnj/bin |
33 #ML_HOME="$ISABELLE_HOME/../smlnj/bin" |
34 #ML_OPTIONS="@SMLdebug=/dev/null" |
34 #ML_OPTIONS="@SMLdebug=/dev/null" |
35 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) |
35 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
36 |
36 |
37 # Moscow ML 2.00 or later (experimental!) |
37 # Moscow ML 2.00 or later (experimental!) |
38 #ML_SYSTEM=mosml |
38 #ML_SYSTEM=mosml |
39 #ML_HOME=$ISABELLE_HOME/../mosml/bin |
39 #ML_HOME="$ISABELLE_HOME/../mosml/bin" |
40 #ML_PLATFORM="" |
40 #ML_PLATFORM="" |
41 #ML_OPTIONS="" |
41 #ML_OPTIONS="" |
42 |
42 |
43 # MLWorks 2.0 |
43 # MLWorks 2.0 |
44 #ML_SYSTEM=mlworks |
44 #ML_SYSTEM=mlworks |
45 #ML_HOME=$ISABELLE_HOME/../mlworks/bin |
45 #ML_HOME="$ISABELLE_HOME/../mlworks/bin" |
46 #ML_OPTIONS="" |
46 #ML_OPTIONS="" |
47 #ML_PLATFORM="" |
47 #ML_PLATFORM="" |
48 |
48 |
49 # Standard ML of New Jersey 0.93 |
49 # Standard ML of New Jersey 0.93 |
50 #ML_SYSTEM=smlnj-0.93 |
50 #ML_SYSTEM=smlnj-0.93 |
81 |
81 |
82 # The place for user configuration, heap files, etc. |
82 # The place for user configuration, heap files, etc. |
83 ISABELLE_HOME_USER=~/isabelle |
83 ISABELLE_HOME_USER=~/isabelle |
84 |
84 |
85 # Where to look for isabelle tools (multiple dirs separated by ':'). |
85 # Where to look for isabelle tools (multiple dirs separated by ':'). |
86 ISABELLE_TOOLS=$ISABELLE_HOME/lib/Tools |
86 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" |
87 |
87 |
88 # Location for temporary files (should be on a local file system). |
88 # Location for temporary files (should be on a local file system). |
89 ISABELLE_TMP_PREFIX=/tmp/isabelle-$USER |
89 ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
90 |
90 |
91 |
91 |
92 # Heap file locations. ML system identifier appended automatically! |
92 # Heap input locations. ML system identifier is included in lookup. |
|
93 ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
93 |
94 |
94 ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps |
95 # Heap output location. ML system identifier is appended automatically later on. |
95 |
|
96 #A hack! Isabelle build tells us to store heaps etc. within the |
|
97 #distribution. |
|
98 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
96 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
99 ISABELLE_OUTPUT=$ISABELLE_HOME/heaps |
97 #Isabelle build tells us to store heaps etc. within the distribution. |
100 ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info |
98 ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" |
|
99 ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" |
101 else |
100 else |
102 ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps |
101 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
103 ISABELLE_BROWSER_INFO=$ISABELLE_HOME_USER/browser_info |
102 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
104 fi |
103 fi |
105 |
104 |
106 # Site settings check -- just to make it a little bit harder to copy this file! |
105 # Site settings check -- just to make it a little bit harder to copy this file! |
107 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
106 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
108 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
107 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
124 |
123 |
125 |
124 |
126 ## Fonts -- how to install the Isabelle X11 fonts (can be tricky!). |
125 ## Fonts -- how to install the Isabelle X11 fonts (can be tricky!). |
127 |
126 |
128 # (1) Get fonts from local (client side) directory: |
127 # (1) Get fonts from local (client side) directory: |
129 ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash" |
128 ISABELLE_INSTALLFONTS="xset fp+ \"$ISABELLE_HOME/lib/fonts\"; xset fp rehash" |
130 |
129 |
131 # (2) Get from font server at Munich or Cambridge: |
130 # (2) Get from font server at Munich or Cambridge: |
132 #ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
131 #ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
133 #ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" |
132 #ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" |
134 |
133 |
144 ISABELLE_INTERFACE=xterm |
143 ISABELLE_INTERFACE=xterm |
145 ISABELLE_XTERM_OPTIONS="" |
144 ISABELLE_XTERM_OPTIONS="" |
146 |
145 |
147 # Emacs running Isamode. |
146 # Emacs running Isamode. |
148 #ISABELLE_INTERFACE=emacs |
147 #ISABELLE_INTERFACE=emacs |
149 ISAMODE_HOME=$ISABELLE_HOME/contrib/Isamode |
148 ISAMODE_HOME="$ISABELLE_HOME/contrib/Isamode" |
150 ISAMODE_OPTIONS="" |
149 ISAMODE_OPTIONS="" |
151 |
150 |
152 # Proof General |
151 # Proof General |
153 ISABELLE_INTERFACE=$(choosefrom \ |
152 ISABELLE_INTERFACE=$(choosefrom \ |
154 "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
153 "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
155 "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
154 "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
|
155 "/usr/share/ProofGeneral/isar/interface" \ |
156 "$ISABELLE_INTERFACE") |
156 "$ISABELLE_INTERFACE") |
157 PROOFGENERAL_OPTIONS="" |
157 PROOFGENERAL_OPTIONS="" |
158 |
158 |
159 # X-Symbol mode for Proof General |
159 # X-Symbol mode for Proof General |
160 XSYMBOL_HOME=$(choosefrom \ |
160 XSYMBOL_HOME=$(choosefrom \ |
161 "$ISABELLE_HOME/contrib/x-symbol" \ |
161 "$ISABELLE_HOME/contrib/x-symbol" \ |
162 "$ISABELLE_HOME/../x-symbol" \ |
162 "$ISABELLE_HOME/../x-symbol" \ |
|
163 "/usr/share/x-symbol" \ |
163 "") |
164 "") |
164 |
165 |
165 |
166 |
166 ### |
167 ### |
167 ### External reasoning tools |
168 ### External reasoning tools |