# HG changeset patch
# User wenzelm
# Date 1492793850 -7200
# Node ID ae09b9f5980bc6c1a81481457935aa2607e705f2
# Parent  2b73ed8bf4d96a44a1c9551ef278edfe295c8218
afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;

diff -r 2b73ed8bf4d9 -r ae09b9f5980b NEWS
--- a/NEWS	Fri Apr 21 18:51:24 2017 +0200
+++ b/NEWS	Fri Apr 21 18:57:30 2017 +0200
@@ -56,9 +56,6 @@
 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 2b73ed8bf4d9 -r ae09b9f5980b src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Apr 21 18:51:24 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri Apr 21 18:57:30 2017 +0200
@@ -231,7 +231,6 @@
 \<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
@@ -258,11 +257,6 @@
   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 2b73ed8bf4d9 -r ae09b9f5980b src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 21 18:51:24 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 21 18:57:30 2017 +0200
@@ -97,7 +97,6 @@
   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"
@@ -134,7 +133,6 @@
 
 # options
 
-JEDIT_ALL_KNOWN=""
 BUILD_ONLY=false
 BUILD_JARS="jars"
 ML_PROCESS_POLICY=""
@@ -147,12 +145,9 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "AD:J:Rbd:fj:l:m:np:s" OPT
+  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
   do
     case "$OPT" in
-      A)
-        JEDIT_ALL_KNOWN="true"
-        ;;
       D)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
         ;;
@@ -376,7 +371,7 @@
 
 if [ "$BUILD_ONLY" = false ]
 then
-  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_ALL_KNOWN JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+  export JEDIT_SESSION_DIRS JEDIT_LOGIC 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[@]}"
diff -r 2b73ed8bf4d9 -r ae09b9f5980b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Apr 21 18:51:24 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 21 18:57:30 2017 +0200
@@ -74,9 +74,8 @@
     val session_name = JEdit_Sessions.session_name(options)
     val session_base =
       try {
-        Sessions.session_base(options, session_name,
-          dirs = JEdit_Sessions.session_dirs(),
-          all_known = Isabelle_System.getenv("JEDIT_ALL_KNOWN") == "true")
+        Sessions.session_base(
+          options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
       }
       catch { case ERROR(_) => Sessions.Base.pure(options) }