src/Tools/jEdit/lib/Tools/jedit
changeset 66574 e16b27bd3f76
parent 66555 39257f39c7da
child 66590 8e1aac4eed11
equal deleted inserted replaced
66573:a6401a6417cf 66574:e16b27bd3f76
   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