# HG changeset patch
# User wenzelm
# Date 1243718857 -7200
# Node ID abab3a577e10c400c02bb06b777f83b6541a3a69
# Parent  aaa147cd92f911c273c1d7353ae8d4ca8973b880
slightly more robust treatment of options via arrays;
tuned;

diff -r aaa147cd92f9 -r abab3a577e10 src/Tools/jEdit/dist-template/interface
--- a/src/Tools/jEdit/dist-template/interface	Sat May 30 12:11:40 2009 +0200
+++ b/src/Tools/jEdit/dist-template/interface	Sat May 30 23:27:37 2009 +0200
@@ -37,14 +37,17 @@
 JEDIT_LOGIC="$ISABELLE_LOGIC"
 JEDIT_PRINT_MODE=""
 
+declare -a JAVA_OPTIONS; eval "JAVA_OPTIONS=($JEDIT_JAVA_OPTIONS)"
+declare -a OPTIONS; eval "OPTIONS=($JEDIT_OPTIONS)"
+
 while getopts "J:j:l:m:" OPT
 do
   case "$OPT" in
     J)
-      JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS $OPTARG"
+      JAVA_OPTIONS+=("$OPTARG")
       ;;
     j)
-      JEDIT_OPTIONS="$JEDIT_OPTIONS $OPTARG"
+      OPTIONS+=("$OPTARG")
       ;;
     l)
       JEDIT_LOGIC="$OPTARG"
@@ -67,13 +70,13 @@
 
 # args
 
-unset FILES; declare -a FILES
+declare -a FILES=()
 
 if [ "$#" -eq 0 ]; then
-  FILES[0]="isabelle:$HOME/Scratch.thy"
+  FILES+=("isabelle:$HOME/Scratch.thy")
 else
   while [ "$#" -gt 0 ]; do
-    FILES[${#FILES[@]}]="isabelle:$1"
+    FILES+=("isabelle:$1")
     shift
   done
 fi
@@ -91,6 +94,6 @@
 
 export JEDIT_LOGIC JEDIT_PRINT_MODE
 
-exec "$ISABELLE_TOOL" java $JEDIT_JAVA_OPTIONS \
+exec "$ISABELLE_TOOL" java "${JAVA_OPTIONS[@]}" \
   -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
-  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS "${FILES[@]}"
+  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${OPTIONS[@]}" "${FILES[@]}"