afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
authorwenzelm
Fri, 21 Apr 2017 18:57:30 +0200
changeset 65541 ae09b9f5980b
parent 65540 2b73ed8bf4d9
child 65542 6a00518bbfcc
afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
NEWS
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/plugin.scala
--- 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
--- 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
--- 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[@]}"
--- 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) }