equal
deleted
inserted
replaced
97 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
97 echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" |
98 echo |
98 echo |
99 echo " Options are:" |
99 echo " Options are:" |
100 echo " -D NAME=X set JVM system property" |
100 echo " -D NAME=X set JVM system property" |
101 echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
101 echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
102 echo " -R open ROOT entry of logic session and use its parent" |
102 echo " -R restrict to parent of logic session and open its ROOT" |
103 echo " -b build only" |
103 echo " -b build only" |
104 echo " -d DIR include session directory" |
104 echo " -d DIR include session directory" |
105 echo " -f fresh build" |
105 echo " -f fresh build" |
106 echo " -j OPTION add jEdit runtime option" |
106 echo " -j OPTION add jEdit runtime option" |
107 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
107 echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" |
135 |
135 |
136 BUILD_ONLY=false |
136 BUILD_ONLY=false |
137 BUILD_JARS="jars" |
137 BUILD_JARS="jars" |
138 ML_PROCESS_POLICY="" |
138 ML_PROCESS_POLICY="" |
139 JEDIT_SESSION_DIRS="" |
139 JEDIT_SESSION_DIRS="" |
140 JEDIT_LOGIC_ROOT="" |
140 JEDIT_LOGIC_RESTRICT="" |
141 JEDIT_LOGIC="" |
141 JEDIT_LOGIC="" |
142 JEDIT_PRINT_MODE="" |
142 JEDIT_PRINT_MODE="" |
143 JEDIT_BUILD_MODE="normal" |
143 JEDIT_BUILD_MODE="normal" |
144 |
144 |
145 function getoptions() |
145 function getoptions() |
153 ;; |
153 ;; |
154 J) |
154 J) |
155 JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
155 JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" |
156 ;; |
156 ;; |
157 R) |
157 R) |
158 JEDIT_LOGIC_ROOT="true" |
158 JEDIT_LOGIC_RESTRICT="true" |
159 ;; |
159 ;; |
160 b) |
160 b) |
161 BUILD_ONLY=true |
161 BUILD_ONLY=true |
162 ;; |
162 ;; |
163 d) |
163 d) |
369 |
369 |
370 ## main |
370 ## main |
371 |
371 |
372 if [ "$BUILD_ONLY" = false ] |
372 if [ "$BUILD_ONLY" = false ] |
373 then |
373 then |
374 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE |
374 export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT JEDIT_PRINT_MODE JEDIT_BUILD_MODE |
375 export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
375 export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" |
376 classpath "$JEDIT_HOME/dist/jedit.jar" |
376 classpath "$JEDIT_HOME/dist/jedit.jar" |
377 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
377 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" |
378 fi |
378 fi |