src/Tools/jEdit/lib/Tools/jedit
changeset 65572 6acb28e5ba41
parent 65541 ae09b9f5980b
child 66120 e03ff7e831cc
equal deleted inserted replaced
65571:923e32ad0976 65572:6acb28e5ba41
    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