# HG changeset patch
# User wenzelm
# Date 1509618337 -3600
# Node ID 7f8c1dd7576a32b4782d3f8163e5440a0a57427f
# Parent  352b23c97ac860f82c7a641eb52f0eb85964d6af
support alternative ancestor session;

diff -r 352b23c97ac8 -r 7f8c1dd7576a NEWS
--- a/NEWS	Thu Nov 02 10:16:22 2017 +0100
+++ b/NEWS	Thu Nov 02 11:25:37 2017 +0100
@@ -34,14 +34,18 @@
 
 * Completion supports theory header imports.
 
-* The command-line tool "isabelle jedit" provides more flexible options:
-  - options -B or -P modify the meaning of -l to produce an image on the
-    spot or use the session parent image
+* The command-line tool "isabelle jedit" provides more flexible options
+for session selection:
+  - options -P opens the parent session image of -l
+  - options -A and -B modify the meaning of -l to produce a base
+    image on the spot, based on the specified ancestor (or parent)
   - option -F focuses on the specified logic session
   - option -R has changed: it only opens the session ROOT entry
   - option -S sets up the development environment to edit the
     specified session: it abbreviates -B -F -R -l
 
+  Example: isabelle jedit -A HOL -S Formal_SSA -d '$AFP'
+
 
 *** HOL ***
 
diff -r 352b23c97ac8 -r 7f8c1dd7576a src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Thu Nov 02 11:25:37 2017 +0100
@@ -228,6 +228,7 @@
 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
 
   Options are:
+    -A           specify ancestor for base session image (default: parent)
     -B           use base session image, with theories from other sessions
     -F           focus on selected logic session: ignore unrelated theories
     -D NAME=X    set JVM system property
@@ -260,15 +261,14 @@
   The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
   session image.
 
-  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.
+  Option \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-B\<close> and are mutually exclusive and modify the meaning of
+  option \<^verbatim>\<open>-l\<close> as follows. Option \<^verbatim>\<open>-P\<close> opens the parent session image. Option
+  \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on the required theory
+  imports from other sessions, relative to an ancestor session given by option
+  \<^verbatim>\<open>-A\<close> (default: parent session).
 
-  Option \<^verbatim>\<open>-F\<close> focuses on the specified logic session, as resulting from
-  options \<^verbatim>\<open>-l\<close>, \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-P\<close>. The accessible name space of theories is
-  restricted to sessions that are connected to this session.
+  Option \<^verbatim>\<open>-F\<close> focuses on the effective logic session: the accessible
+  namespace of theories is restricted to sessions that are connected to it.
 
   Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
   editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
diff -r 352b23c97ac8 -r 7f8c1dd7576a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 11:25:37 2017 +0100
@@ -152,6 +152,7 @@
   {
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
+    def get(name: String): Option[Base] = session_bases.get(name)
 
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
@@ -337,6 +338,7 @@
 
   def base_info(options: Options, session: String,
     dirs: List[Path] = Nil,
+    ancestor_session: Option[String] = None,
     all_known: Boolean = false,
     focus_session: Boolean = false,
     required_session: Boolean = false): Base_Info =
@@ -346,24 +348,30 @@
 
     val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
     val info = selected_sessions(session)
+    val ancestor = ancestor_session orElse info.parent
 
     val (session1, infos1) =
-      if (required_session && info.parent.isDefined) {
+      if (required_session && ancestor.isDefined) {
         val deps = Sessions.deps(selected_sessions, global_theories)
         val base = deps(session)
 
-        val parent_loaded = deps(info.parent.get).loaded_theories.defined(_)
+        val ancestor_loaded =
+          deps.get(ancestor.get) match {
+            case None =>
+              error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
+            case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
+          }
 
         val required_theories =
           for {
             thy <- base.loaded_theories.keys
-            if !parent_loaded(thy) && base.theory_qualifier(thy) != session
+            if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
           }
           yield thy
 
-        if (required_theories.isEmpty) (info.parent.get, Nil)
+        if (required_theories.isEmpty) (ancestor.get, Nil)
         else {
-          val other_name = info.name + "(base)"
+          val other_name = info.name + "_base(" + ancestor.get + ")"
           (other_name,
             List(
               make_info(info.options,
@@ -375,7 +383,7 @@
                   name = other_name,
                   groups = info.groups,
                   path = ".",
-                  parent = info.parent,
+                  parent = ancestor,
                   description = "Required theory imports from other sessions",
                   options = Nil,
                   imports = info.imports,
diff -r 352b23c97ac8 -r 7f8c1dd7576a src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Nov 02 11:25:37 2017 +0100
@@ -97,6 +97,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
   echo
   echo "  Options are:"
+  echo "    -A           specify ancestor for base session image (default: parent)"
   echo "    -B           use base session image, with theories from other sessions"
   echo "    -F           focus on selected logic session: ignore unrelated theories"
   echo "    -D NAME=X    set JVM system property"
@@ -141,6 +142,7 @@
 BUILD_ONLY=false
 BUILD_JARS="jars"
 ML_PROCESS_POLICY=""
+JEDIT_LOGIC_ANCESTOR=""
 JEDIT_LOGIC_BASE=""
 JEDIT_LOGIC_FOCUS=""
 JEDIT_SESSION_DIRS=""
@@ -153,9 +155,12 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "BFD:J:PRS:bd:fj:l:m:np:s" OPT
+  while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
+      A)
+        JEDIT_LOGIC_ANCESTOR="$OPTARG"
+        ;;
       B)
         JEDIT_LOGIC_BASE="true"
         JEDIT_LOGIC_PARENT=""
@@ -424,7 +429,7 @@
 
 if [ "$BUILD_ONLY" = false ]
 then
-  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
+  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
     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"
diff -r 352b23c97ac8 -r 7f8c1dd7576a src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 11:25:37 2017 +0100
@@ -39,6 +39,7 @@
       Isabelle_System.getenv("JEDIT_LOGIC"),
       options.string(jedit_logic_option))
 
+  def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
   def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
   def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
   def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
@@ -109,6 +110,7 @@
         if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
         else logic_name(options),
       dirs = JEdit_Sessions.session_dirs(),
+      ancestor_session = logic_ancestor,
       all_known = !logic_focus,
       focus_session = logic_focus,
       required_session = logic_base)