src/Tools/jEdit/lib/Tools/jedit
changeset 65572 6acb28e5ba41
parent 65541 ae09b9f5980b
child 66120 e03ff7e831cc
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Apr 24 11:05:24 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Apr 24 11:23:07 2017 +0200
@@ -99,7 +99,7 @@
   echo "  Options are:"
   echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
-  echo "    -R           open ROOT entry of logic session and use its parent"
+  echo "    -R           restrict to parent of logic session and open its ROOT"
   echo "    -b           build only"
   echo "    -d DIR       include session directory"
   echo "    -f           fresh build"
@@ -137,7 +137,7 @@
 BUILD_JARS="jars"
 ML_PROCESS_POLICY=""
 JEDIT_SESSION_DIRS=""
-JEDIT_LOGIC_ROOT=""
+JEDIT_LOGIC_RESTRICT=""
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
 JEDIT_BUILD_MODE="normal"
@@ -155,7 +155,7 @@
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;
       R)
-        JEDIT_LOGIC_ROOT="true"
+        JEDIT_LOGIC_RESTRICT="true"
         ;;
       b)
         BUILD_ONLY=true
@@ -371,7 +371,7 @@
 
 if [ "$BUILD_ONLY" = false ]
 then
-  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
   classpath "$JEDIT_HOME/dist/jedit.jar"
   exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"