refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
authorwenzelm
Wed, 17 Nov 2010 13:38:53 +0100
changeset 40574 226563829580
parent 40573 113ccf02d323
child 40581 4e10046d7aaa
refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
src/Tools/jEdit/dist-template/lib/Tools/jedit
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Nov 17 11:24:07 2010 +0100
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Nov 17 13:38:53 2010 +0100
@@ -24,7 +24,6 @@
   echo "    -m MODE      add print mode for output"
   echo
   echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
-  echo "(default ~/Scratch.thy)."
   echo
   exit 1
 }
@@ -93,14 +92,10 @@
 
 # args
 
-if [ "$#" -eq 0 ]; then
-  ARGS["${#ARGS[@]}"]="Scratch.thy"
-else
-  while [ "$#" -gt 0 ]; do
-    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
-    shift
-  done
-fi
+while [ "$#" -gt 0 ]; do
+  ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+  shift
+done
 
 
 ## default perspective