equal
deleted
inserted
replaced
96 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
96 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
97 echo |
97 echo |
98 echo " Options are:" |
98 echo " Options are:" |
99 echo " -D NAME=X set JVM system property" |
99 echo " -D NAME=X set JVM system property" |
100 echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
100 echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
|
101 echo " -R open ROOT entry of logic session and use its parent" |
101 echo " -b build only" |
102 echo " -b build only" |
102 echo " -d DIR include session directory" |
103 echo " -d DIR include session directory" |
103 echo " -f fresh build" |
104 echo " -f fresh build" |
104 echo " -j OPTION add jEdit runtime option" |
105 echo " -j OPTION add jEdit runtime option" |
105 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
106 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
133 |
134 |
134 BUILD_ONLY=false |
135 BUILD_ONLY=false |
135 BUILD_JARS="jars" |
136 BUILD_JARS="jars" |
136 ML_PROCESS_POLICY="" |
137 ML_PROCESS_POLICY="" |
137 JEDIT_SESSION_DIRS="" |
138 JEDIT_SESSION_DIRS="" |
|
139 JEDIT_LOGIC_ROOT="" |
138 JEDIT_LOGIC="" |
140 JEDIT_LOGIC="" |
139 JEDIT_PRINT_MODE="" |
141 JEDIT_PRINT_MODE="" |
140 JEDIT_BUILD_MODE="normal" |
142 JEDIT_BUILD_MODE="normal" |
141 |
143 |
142 function getoptions() |
144 function getoptions() |
143 { |
145 { |
144 OPTIND=1 |
146 OPTIND=1 |
145 while getopts "D:J:bd:fj:l:m:np:s" OPT |
147 while getopts "D:J:Rbd:fj:l:m:np:s" OPT |
146 do |
148 do |
147 case "$OPT" in |
149 case "$OPT" in |
148 D) |
150 D) |
149 JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" |
151 JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" |
150 ;; |
152 ;; |
151 J) |
153 J) |
152 JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
154 JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
|
155 ;; |
|
156 R) |
|
157 JEDIT_LOGIC_ROOT="true" |
153 ;; |
158 ;; |
154 b) |
159 b) |
155 BUILD_ONLY=true |
160 BUILD_ONLY=true |
156 ;; |
161 ;; |
157 d) |
162 d) |
363 |
368 |
364 ## main |
369 ## main |
365 |
370 |
366 if [ "$BUILD_ONLY" = false ] |
371 if [ "$BUILD_ONLY" = false ] |
367 then |
372 then |
368 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE |
373 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE |
369 export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
374 export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
370 classpath "$JEDIT_HOME/dist/jedit.jar" |
375 classpath "$JEDIT_HOME/dist/jedit.jar" |
371 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
376 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
372 fi |
377 fi |