# HG changeset patch
# User wenzelm
# Date 1250953686 -7200
# Node ID 468eff174a77ab3f1b9af6b9774d2a7087f85ab5
# Parent  cb3c5189ea8568040a7cd5f5ab57c4c4723c3270
function splitarray: splightly more abstract version that accomodates older bashes;

diff -r cb3c5189ea85 -r 468eff174a77 bin/isabelle
--- a/bin/isabelle	Fri Aug 21 19:06:12 2009 +0200
+++ b/bin/isabelle	Sat Aug 22 17:08:06 2009 +0200
@@ -17,7 +17,7 @@
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
-ORIG_IFS="$IFS"; IFS=":"; declare -a TOOLS=($ISABELLE_TOOLS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
 
 
 ## diagnostics
diff -r cb3c5189ea85 -r 468eff174a77 bin/isabelle-process
--- a/bin/isabelle-process	Fri Aug 21 19:06:12 2009 +0200
+++ b/bin/isabelle-process	Sat Aug 22 17:08:06 2009 +0200
@@ -160,7 +160,7 @@
     INFILE=""
     ISA_PATH=""
 
-    ORIG_IFS="$IFS"; IFS=":"; declare -a PATHS=($ISABELLE_PATH); IFS="$ORIG_IFS"
+    splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
     for DIR in "${PATHS[@]}"
     do
       DIR="$DIR/$ML_IDENTIFIER"
diff -r cb3c5189ea85 -r 468eff174a77 lib/Tools/doc
--- a/lib/Tools/doc	Fri Aug 21 19:06:12 2009 +0200
+++ b/lib/Tools/doc	Sat Aug 22 17:08:06 2009 +0200
@@ -34,7 +34,7 @@
 
 ## main
 
-ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}")
 
 if [ -z "$DOC" ]; then
   for DIR in "${DOCS[@]}"
diff -r cb3c5189ea85 -r 468eff174a77 lib/Tools/document
--- a/lib/Tools/document	Fri Aug 21 19:06:12 2009 +0200
+++ b/lib/Tools/document	Sat Aug 22 17:08:06 2009 +0200
@@ -53,7 +53,7 @@
       OUTFORMAT="$OPTARG"
       ;;
     t)
-      ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS"
+      splitarray "," "$OPTARG"; TAGS=("${SPLITARRAY[@]}")
       ;;
     \?)
       usage
diff -r cb3c5189ea85 -r 468eff174a77 lib/Tools/findlogics
--- a/lib/Tools/findlogics	Fri Aug 21 19:06:12 2009 +0200
+++ b/lib/Tools/findlogics	Sat Aug 22 17:08:06 2009 +0200
@@ -25,7 +25,7 @@
 declare -a LOGICS=()
 declare -a ISABELLE_PATHS=()
 
-ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS
+splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
 
 for DIR in "${ISABELLE_PATHS[@]}"
 do
diff -r cb3c5189ea85 -r 468eff174a77 lib/Tools/makeall
--- a/lib/Tools/makeall	Fri Aug 21 19:06:12 2009 +0200
+++ b/lib/Tools/makeall	Sat Aug 22 17:08:06 2009 +0200
@@ -34,7 +34,7 @@
 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
-ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_COMPONENTS"; COMPONENTS=("${SPLITARRAY[@]}")
 
 for DIR in "${COMPONENTS[@]}"
 do
diff -r cb3c5189ea85 -r 468eff174a77 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Fri Aug 21 19:06:12 2009 +0200
+++ b/lib/scripts/getsettings	Sat Aug 22 17:08:06 2009 +0200
@@ -68,6 +68,17 @@
   done
 }
 
+#arrays
+function splitarray ()
+{
+  SPLITARRAY=()
+  local IFS="$1"; shift
+  for X in $*
+  do
+    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
+  done
+}
+
 #nested components
 ISABELLE_COMPONENTS=""
 function init_component ()