# HG changeset patch
# User wenzelm
# Date 1493025787 -7200
# Node ID 6acb28e5ba4176c163dd6956e4388bb065d99716
# Parent  923e32ad09764b582ecfc1bd28243476bfaa3aef
clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;

diff -r 923e32ad0976 -r 6acb28e5ba41 NEWS
--- a/NEWS	Mon Apr 24 11:05:24 2017 +0200
+++ b/NEWS	Mon Apr 24 11:23:07 2017 +0200
@@ -52,9 +52,10 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
-* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
-entry of the specified logic session in the editor, while its parent is
-used for formal checking.
+* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
+image of the SESSION, with qualified theory imports restricted to that
+portion of the session graph. Moreover, the ROOT entry of the SESSION is
+opened in the editor.
 
 * The PIDE document model maintains file content independently of the
 status of jEdit editor buffers. Reloading jEdit buffers no longer causes
diff -r 923e32ad0976 -r 6acb28e5ba41 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Apr 24 11:05:24 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Apr 24 11:23:07 2017 +0200
@@ -233,7 +233,7 @@
   Options are:
     -D NAME=X    set JVM system property
     -J OPTION    add JVM runtime option
-    -R           open ROOT entry of logic session and use its parent
+    -R           restrict to parent of logic session and open its ROOT
     -b           build only
     -d DIR       include session directory
     -f           fresh build
@@ -257,10 +257,12 @@
   The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
   session image.
 
-  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
-  entry of the specified session is opened in the editor, while its parent
-  session is used for formal checking. This facilitates maintenance of a
-  broken session, by moving the Prover IDE quickly to relevant source files.
+  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close>~\<open>session\<close> as follows: the
+  parent image of the \<open>session\<close> is used, with qualified theory imports
+  restricted to that portion of the session graph. Moreover, the \<^verbatim>\<open>ROOT\<close> entry
+  of the \<open>session\<close> is opened in the editor. This facilitates maintenance of a
+  particular session, by moving the Prover IDE quickly to relevant source
+  files.
 
   The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
   Note that the system option @{system_option_ref jedit_print_mode} allows to
diff -r 923e32ad0976 -r 6acb28e5ba41 src/Tools/jEdit/lib/Tools/jedit
--- 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[@]}"
diff -r 923e32ad0976 -r 6acb28e5ba41 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:05:24 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:23:07 2017 +0200
@@ -30,6 +30,9 @@
       case s => options.string("ML_process_policy") = s
     }
 
+  def session_restricted(): Boolean =
+    Isabelle_System.getenv("JEDIT_LOGIC_RESTRICT") == "true"
+
   def session_info(options: Options): Info =
   {
     val logic =
@@ -43,16 +46,19 @@
         catch { case ERROR(_) => None }
       info <- sessions.get(logic)
       parent <- info.parent
-      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
+      if session_restricted()
     } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
   }
 
   def session_name(options: Options): String = session_info(options).name
 
   def session_base(options: Options): Sessions.Base =
+  {
+    val all_known = !session_restricted()
     Sessions.session_base(
-      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
+      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
     .platform_path
+  }
 
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")