back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;

--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 26 22:14:12 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Aug 26 22:25:41 2011 +0200
@@ -134,11 +134,14 @@
 
 # args
 
-while [ "$#" -gt 0 ]
-do
-  ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
-  shift
-done
+if [ "$#" -eq 0 ]; then
+  ARGS["${#ARGS[@]}"]="Scratch.thy"
+else
+  while [ "$#" -gt 0 ]; do
+    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+    shift
+  done
+fi
 
 
 ## dependencies