# HG changeset patch
# User wenzelm
# Date 1492611899 -7200
# Node ID ea42dfd95ec83b11608812bf6e3c13c3a7506b68
# Parent  da387a5d4b0916867dc794552d453ab942ca140e
optionally explore all sessions -- potentially slow, e.g. for AFP;

diff -r da387a5d4b09 -r ea42dfd95ec8 NEWS
--- a/NEWS	Wed Apr 19 16:22:20 2017 +0200
+++ b/NEWS	Wed Apr 19 16:24:59 2017 +0200
@@ -56,6 +56,9 @@
 entry of the specified logic session in the editor, while its parent is
 used for formal checking.
 
+* Improved support for editing of a complex session hierarchy with
+session-qualified theory imports: "isabelle jedit -A".
+
 * The PIDE document model maintains file content independently of the
 status of jEdit editor buffers. Reloading jEdit buffers no longer causes
 changes of formal document content. Theory dependencies are always
diff -r da387a5d4b09 -r ea42dfd95ec8 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Apr 19 16:22:20 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Apr 19 16:24:59 2017 +0200
@@ -231,6 +231,7 @@
 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
 
   Options are:
+    -A           explore theory imports of all known sessions
     -D NAME=X    set JVM system property
     -J OPTION    add JVM runtime option
     -R           open ROOT entry of logic session and use its parent
@@ -257,6 +258,11 @@
   The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
   session image.
 
+  Option \<^verbatim>\<open>-A\<close> explores theory imports of all known sessions (according to the
+  directories specified via option \<^verbatim>\<open>-d\<close>). This facilitates editing of a
+  complex session hierarchy with session-qualified theory imports, while using
+  a different base session image than usual.
+
   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
diff -r da387a5d4b09 -r ea42dfd95ec8 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Apr 19 16:22:20 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Apr 19 16:24:59 2017 +0200
@@ -97,6 +97,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
   echo
   echo "  Options are:"
+  echo "    -A           explore theory imports of all known sessions"
   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"
@@ -133,6 +134,7 @@
 
 # options
 
+JEDIT_ALL_KNOWN=""
 BUILD_ONLY=false
 BUILD_JARS="jars"
 ML_PROCESS_POLICY=""
@@ -145,9 +147,12 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
+  while getopts "AD:J:Rbd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
+      A)
+        JEDIT_ALL_KNOWN="true"
+        ;;
       D)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
         ;;
@@ -371,7 +376,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_ROOT JEDIT_ALL_KNOWN 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 da387a5d4b09 -r ea42dfd95ec8 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Apr 19 16:22:20 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Apr 19 16:24:59 2017 +0200
@@ -73,7 +73,11 @@
     val options = this.options.value
     val session_name = JEdit_Sessions.session_name(options)
     val session_base =
-      try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
+      try {
+        Sessions.session_base(options, session_name,
+          dirs = JEdit_Sessions.session_dirs(),
+          all_known = Isabelle_System.getenv("JEDIT_ALL_KNOWN") == "true")
+      }
       catch { case ERROR(_) => Sessions.Base.pure(options) }
 
     _resources = new JEdit_Resources(session_base.platform_path)