diff -r 0e49a2edadea -r c60770179a0c src/Tools/jEdit/dist-template/interface
--- a/src/Tools/jEdit/dist-template/interface	Fri Dec 19 23:56:58 2008 +0100
+++ b/src/Tools/jEdit/dist-template/interface	Sat Dec 20 00:14:25 2008 +0100
@@ -67,12 +67,13 @@
 
 # args
 
-FILES=""
+unset FILES; declare -a FILES
+
 if [ "$#" -eq 0 ]; then
-  FILES="isabelle:$HOME/Scratch.thy"
+  FILES[0]="isabelle:$HOME/Scratch.thy"
 else
   while [ "$#" -gt 0 ]; do
-    FILES="$FILES isabelle:$1"
+    FILES[${#FILES[@]}]="isabelle:$1"
     shift
   done
 fi
@@ -92,4 +93,4 @@
 
 exec "$ISABELLE_TOOL" java $JEDIT_JAVA_OPTIONS \
   -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
-  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS $FILES
+  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS "${FILES[@]}"