src/Tools/jEdit/lib/Tools/jedit
changeset 64602 8edca3465758
parent 63987 ac96fe9224f6
child 64621 7116f2634e32
equal deleted inserted replaced
64601:37ce6ceacbb7 64602:8edca3465758
    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