equal
deleted
inserted
replaced
67 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
67 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
68 echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" |
68 echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" |
69 echo " -m MODE add print mode for output" |
69 echo " -m MODE add print mode for output" |
70 echo |
70 echo |
71 echo "Start jEdit with Isabelle plugin setup and opens theory FILES" |
71 echo "Start jEdit with Isabelle plugin setup and opens theory FILES" |
72 echo "(default Scratch.thy)." |
72 echo "(default \"$USER_HOME/Scratch.thy\")." |
73 echo |
73 echo |
74 exit 1 |
74 exit 1 |
75 } |
75 } |
76 |
76 |
77 function fail() |
77 function fail() |
151 |
151 |
152 |
152 |
153 # args |
153 # args |
154 |
154 |
155 if [ "$#" -eq 0 ]; then |
155 if [ "$#" -eq 0 ]; then |
156 ARGS["${#ARGS[@]}"]="Scratch.thy" |
156 ARGS["${#ARGS[@]}"]="$USER_HOME/Scratch.thy" |
157 else |
157 else |
158 while [ "$#" -gt 0 ]; do |
158 while [ "$#" -gt 0 ]; do |
159 ARGS["${#ARGS[@]}"]="$(jvmpath "$1")" |
159 ARGS["${#ARGS[@]}"]="$(jvmpath "$1")" |
160 shift |
160 shift |
161 done |
161 done |