tuned/clarified some component settings;
explicit comments about common mistakes;
--- a/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_SUM_OF_SQUARES="$COMPONENT"
--- a/src/HOL/Mirabelle/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Mirabelle/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
MIRABELLE_HOME="$COMPONENT"
MIRABELLE_LOGIC=HOL
@@ -5,4 +7,4 @@
MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
MIRABELLE_TIMEOUT=30
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Mutabelle/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,7 +1,9 @@
+# -*- shell-script -*- :mode=shellscript:
+
MUTABELLE_HOME="$COMPONENT"
DEFAULT_MUTABELLE_LOGIC=HOL
DEFAULT_MUTABELLE_IMPORT_THEORY=Complex_Main
DEFAULT_MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Tools/ATP/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Tools/ATP/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_ATP="$COMPONENT"
--- a/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,5 +1,8 @@
# -*- shell-script -*- :mode=shellscript:
+# FIXME contrib_devel not official
+# FIXME $(type -p swipl) etc. does not allow spaces in file name
+
EXEC_SWIPL="$(choosefrom \
"$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \
"$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \
--- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 15:19:15 2010 +0100
@@ -7,6 +7,9 @@
if [ "$EXEC_SWIPL" = "" ]; then
echo ""
else
+ # FIXME does not allow spaces in $EXEC_SWIPL
+ # FIXME "expr match" not portable
+ # FIXME prefer $(...) in bash
VERSION=`$EXEC_SWIPL --version`
echo `expr match "$VERSION" 'SWI-Prolog version \([0-9\.]*\)'`
fi
--- a/src/HOL/Tools/SMT/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/HOL/Tools/SMT/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_SMT="$COMPONENT"
REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt"
--- a/src/Tools/WWW_Find/etc/settings Mon Dec 20 14:44:00 2010 +0100
+++ b/src/Tools/WWW_Find/etc/settings Mon Dec 20 15:19:15 2010 +0100
@@ -1,7 +1,8 @@
-# the path to lighttpd
+# -*- shell-script -*- :mode=shellscript:
+
LIGHTTPD="/usr/sbin/lighttpd"
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-
WWWFINDDIR="$COMPONENT"
WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"