added isabelle jedit options -B, -P, clarified -R;
misc tuning and clarification;

--- a/NEWS	Wed Nov 01 13:06:01 2017 +0100
+++ b/NEWS	Wed Nov 01 15:32:07 2017 +0100
@@ -34,6 +34,10 @@
 
 * Completion supports theory header imports.
 
+* The "isabelle jedit" command-line options -B or -P modify the meaning
+of -l to produce an image on the spot or use the session parent image.
+Option -R now only opens the session ROOT entry.
+
 
 *** HOL ***
 

--- a/src/Doc/JEdit/JEdit.thy	Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Nov 01 15:32:07 2017 +0100
@@ -228,10 +228,12 @@
 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
 
   Options are:
+    -B           use image with required theory imports from other sessions
     -D NAME=X    set JVM system property
     -J OPTION    add JVM runtime option
                  (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
-    -R           open ROOT entry of logic session and use its parent
+    -P           use parent session image
+    -R           open ROOT entry of logic session
     -b           build only
     -d DIR       include session directory
     -f           fresh build
@@ -256,10 +258,11 @@
   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>-B\<close> and \<^verbatim>\<open>-P\<close> are mutually exclusive and modify the meaning of
+  option \<^verbatim>\<open>-l\<close> as follows: \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on
+  the required theory imports from other sessions, or the parent session image
+  if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
+  session image directly.
 
   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
@@ -274,6 +277,9 @@
   The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
   directly to the underlying \<^verbatim>\<open>java\<close> process.
 
+  Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
+  editor.
+
   The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
   Isabelle/jEdit. This is only relevant for building from sources, which also
   requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from

--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Nov 01 15:32:07 2017 +0100
@@ -97,10 +97,12 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
   echo
   echo "  Options are:"
+  echo "    -B           use image with required theory imports from other sessions"
   echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option"
   echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
-  echo "    -R           open ROOT entry of logic session and use its parent"
+  echo "    -P           use parent session image"
+  echo "    -R           open ROOT entry of logic session"
   echo "    -b           build only"
   echo "    -d DIR       include session directory"
   echo "    -f           fresh build"
@@ -137,8 +139,10 @@
 BUILD_ONLY=false
 BUILD_JARS="jars"
 ML_PROCESS_POLICY=""
+JEDIT_LOGIC_BASE=""
 JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC_ROOT=""
+JEDIT_LOGIC_PARENT=""
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
 JEDIT_BUILD_MODE="normal"
@@ -146,15 +150,23 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
+  while getopts "BD:J:PRbd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
+      B)
+        JEDIT_LOGIC_BASE="true"
+        JEDIT_LOGIC_PARENT=""
+        ;;
       D)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
         ;;
       J)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;
+      P)
+        JEDIT_LOGIC_PARENT="true"
+        JEDIT_LOGIC_BASE=""
+        ;;
       R)
         JEDIT_LOGIC_ROOT="true"
         ;;
@@ -399,7 +411,8 @@
 
 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_BASE JEDIT_LOGIC_PARENT \
+    JEDIT_LOGIC_ROOT 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[@]}"

--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Nov 01 15:32:07 2017 +0100
@@ -27,9 +27,10 @@
     new JEdit_Resources(JEdit_Sessions.session_base_info(options))
 }
 
-class JEdit_Resources private(session_base_info: Sessions.Base_Info)
+class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
   extends Resources(session_base_info.base.platform_path)
 {
+  def session_name: String = session_base_info.session
   def session_errors: List[String] = session_base_info.errors
 
 

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 15:32:07 2017 +0100
@@ -16,47 +16,56 @@
 
 object JEdit_Sessions
 {
-  /* session info */
-
-  private val option_name = "jedit_logic"
-
-  sealed case class Info(name: String, open_root: Position.T)
-
-  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+  /* session options */
 
   def session_options(options: Options): Options =
     Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
       case "" => options
-      case s => options.string("ML_process_policy") = s
+      case s => options.string.update("ML_process_policy", s)
     }
 
-  def session_info(options: Options): Info =
-  {
-    val logic =
-      Isabelle_System.default_logic(
-        Isabelle_System.getenv("JEDIT_LOGIC"),
-        options.string(option_name))
+  def session_dirs(): List[Path] =
+    Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+
+  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+
+
+  /* raw logic info */
+
+  private val jedit_logic_option = "jedit_logic"
+
+  def logic_name(options: Options): String =
+    Isabelle_System.default_logic(
+      Isabelle_System.getenv("JEDIT_LOGIC"),
+      options.string(jedit_logic_option))
 
-    (for {
-      sessions <-
-        try { Some(Sessions.load(session_options(options), dirs = session_dirs())) }
-        catch { case ERROR(_) => None }
-      info <- sessions.get(logic)
-      parent <- info.parent
-      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
-    } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
-  }
+  def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
+  def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
+
+  def logic_info(options: Options): Option[Sessions.Info] =
+    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
+    catch { case ERROR(_) => None }
 
-  def session_name(options: Options): String = session_info(options).name
+  def logic_root(options: Options): Position.T =
+    if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
+      logic_info(options).map(_.pos) getOrElse Position.none
+    }
+    else Position.none
+
+
+  /* session base info */
 
   def session_base_info(options: Options): Sessions.Base_Info =
   {
+    val logic = logic_name(options)
+
     Sessions.session_base_info(options,
-      session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
+      if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic,
+      dirs = JEdit_Sessions.session_dirs(),
+      all_known = true,
+      required_session = logic_base)
   }
 
-  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
-
   def session_build(
     options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
   {
@@ -64,24 +73,26 @@
 
     Build.build(options = session_options(options), progress = progress,
       build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
-      dirs = session_dirs(), sessions = List(session_name(options))).rc
+      dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
+      sessions = List(PIDE.resources.session_name)).rc
   }
 
   def session_start(options: Options)
   {
-    val modes =
-      (space_explode(',', options.string("jedit_print_mode")) :::
-       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
-
     Isabelle_Process.start(PIDE.session, session_options(options),
-      logic = session_name(options), dirs = session_dirs(), modes = modes,
+      sessions = Some(PIDE.resources.session_base_info.sessions),
+      logic = PIDE.resources.session_name,
       store = Sessions.store(session_build_mode() == "system"),
+      modes =
+        (space_explode(',', options.string("jedit_print_mode")) :::
+         space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
       phase_changed = PIDE.plugin.session_phase_changed)
   }
 
   def session_list(options: Options): List[String] =
   {
-    val sessions = Sessions.load(options, dirs = session_dirs())
+    val sessions =
+      Sessions.load(options, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos)
     val (main_sessions, other_sessions) =
       sessions.imports_topological_order.partition(info => info.groups.contains("main"))
     main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
@@ -100,21 +111,21 @@
     GUI_Thread.require {}
 
     val entries =
-      new Logic_Entry("", "default (" + session_name(options.value) + ")") ::
+      new Logic_Entry("", "default (" + PIDE.resources.session_name + ")") ::
         session_list(options.value).map(name => new Logic_Entry(name, name))
 
     val component = new ComboBox(entries) with Option_Component {
-      name = option_name
+      name = jedit_logic_option
       val title = "Logic"
       def load: Unit =
       {
-        val logic = options.string(option_name)
+        val logic = options.string(jedit_logic_option)
         entries.find(_.name == logic) match {
           case Some(entry) => selection.item = entry
           case None =>
         }
       }
-      def save: Unit = options.string(option_name) = selection.item.name
+      def save: Unit = options.string(jedit_logic_option) = selection.item.name
     }
 
     component.load()

--- a/src/Tools/jEdit/src/plugin.scala	Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 01 15:32:07 2017 +0100
@@ -322,7 +322,7 @@
           init_view(view)
 
           PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
-            JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
+            JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>

--- a/src/Tools/jEdit/src/session_build.scala	Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Wed Nov 01 15:32:07 2017 +0100
@@ -167,7 +167,7 @@
     setVisible(true)
 
     Standard_Thread.fork("session_build") {
-      progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name(options) + " ...")
+      progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
 
       val (out, rc) =
         try { ("", JEdit_Sessions.session_build(options, progress = progress)) }