equal
deleted
inserted
replaced
108 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
108 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
109 echo |
109 echo |
110 echo " Options are:" |
110 echo " Options are:" |
111 echo " -D NAME=X set JVM system property" |
111 echo " -D NAME=X set JVM system property" |
112 echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
112 echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
113 echo " -R restrict to parent of logic session and open its ROOT" |
113 echo " -R open ROOT entry of logic session and use its parent" |
114 echo " -b build only" |
114 echo " -b build only" |
115 echo " -d DIR include session directory" |
115 echo " -d DIR include session directory" |
116 echo " -f fresh build" |
116 echo " -f fresh build" |
117 echo " -j OPTION add jEdit runtime option" |
117 echo " -j OPTION add jEdit runtime option" |
118 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
118 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
146 |
146 |
147 BUILD_ONLY=false |
147 BUILD_ONLY=false |
148 BUILD_JARS="jars" |
148 BUILD_JARS="jars" |
149 ML_PROCESS_POLICY="" |
149 ML_PROCESS_POLICY="" |
150 JEDIT_SESSION_DIRS="" |
150 JEDIT_SESSION_DIRS="" |
151 JEDIT_LOGIC_RESTRICT="" |
151 JEDIT_LOGIC_ROOT="" |
152 JEDIT_LOGIC="" |
152 JEDIT_LOGIC="" |
153 JEDIT_PRINT_MODE="" |
153 JEDIT_PRINT_MODE="" |
154 JEDIT_BUILD_MODE="normal" |
154 JEDIT_BUILD_MODE="normal" |
155 |
155 |
156 function getoptions() |
156 function getoptions() |
164 ;; |
164 ;; |
165 J) |
165 J) |
166 JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
166 JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
167 ;; |
167 ;; |
168 R) |
168 R) |
169 JEDIT_LOGIC_RESTRICT="true" |
169 JEDIT_LOGIC_ROOT="true" |
170 ;; |
170 ;; |
171 b) |
171 b) |
172 BUILD_ONLY=true |
172 BUILD_ONLY=true |
173 ;; |
173 ;; |
174 d) |
174 d) |
406 |
406 |
407 ## main |
407 ## main |
408 |
408 |
409 if [ "$BUILD_ONLY" = false ] |
409 if [ "$BUILD_ONLY" = false ] |
410 then |
410 then |
411 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT JEDIT_PRINT_MODE JEDIT_BUILD_MODE |
411 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE |
412 export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
412 export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
413 classpath "$JEDIT_HOME/dist/jedit.jar" |
413 classpath "$JEDIT_HOME/dist/jedit.jar" |
414 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
414 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
415 fi |
415 fi |