# HG changeset patch
# User wenzelm
# Date 1292854755 -3600
# Node ID 9e576ec5c0dcbd8f8bb2ea91deb9f38555e7fdb9
# Parent  bb8468ae414eb737cee62e5bd90fcf32d6440acf
tuned/clarified some component settings;
explicit comments about common mistakes;

diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Library/Sum_Of_Squares/etc/settings
--- 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"
diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Mirabelle/etc/settings
--- 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"
diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Mutabelle/etc/settings
--- 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"
diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/ATP/etc/settings
--- 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"
diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/Predicate_Compile/etc/settings
--- 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" \
diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version
--- 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
diff -r bb8468ae414e -r 9e576ec5c0dc src/HOL/Tools/SMT/etc/settings
--- 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"
diff -r bb8468ae414e -r 9e576ec5c0dc src/Tools/WWW_Find/etc/settings
--- 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"