--- 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[@]}"