afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
authorwenzelm
Fri Apr 21 18:57:30 2017 +0200 (2017-04-21)
changeset 65541ae09b9f5980b
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
     1.1 --- a/NEWS	Fri Apr 21 18:51:24 2017 +0200
     1.2 +++ b/NEWS	Fri Apr 21 18:57:30 2017 +0200
     1.3 @@ -56,9 +56,6 @@
     1.4  entry of the specified logic session in the editor, while its parent is
     1.5  used for formal checking.
     1.6  
     1.7 -* Improved support for editing of a complex session hierarchy with
     1.8 -session-qualified theory imports: "isabelle jedit -A".
     1.9 -
    1.10  * The PIDE document model maintains file content independently of the
    1.11  status of jEdit editor buffers. Reloading jEdit buffers no longer causes
    1.12  changes of formal document content. Theory dependencies are always
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Fri Apr 21 18:51:24 2017 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Apr 21 18:57:30 2017 +0200
     2.3 @@ -231,7 +231,6 @@
     2.4  \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
     2.5  
     2.6    Options are:
     2.7 -    -A           explore theory imports of all known sessions
     2.8      -D NAME=X    set JVM system property
     2.9      -J OPTION    add JVM runtime option
    2.10      -R           open ROOT entry of logic session and use its parent
    2.11 @@ -258,11 +257,6 @@
    2.12    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    2.13    session image.
    2.14  
    2.15 -  Option \<^verbatim>\<open>-A\<close> explores theory imports of all known sessions (according to the
    2.16 -  directories specified via option \<^verbatim>\<open>-d\<close>). This facilitates editing of a
    2.17 -  complex session hierarchy with session-qualified theory imports, while using
    2.18 -  a different base session image than usual.
    2.19 -
    2.20    Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    2.21    entry of the specified session is opened in the editor, while its parent
    2.22    session is used for formal checking. This facilitates maintenance of a
     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 21 18:51:24 2017 +0200
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 21 18:57:30 2017 +0200
     3.3 @@ -97,7 +97,6 @@
     3.4    echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
     3.5    echo
     3.6    echo "  Options are:"
     3.7 -  echo "    -A           explore theory imports of all known sessions"
     3.8    echo "    -D NAME=X    set JVM system property"
     3.9    echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
    3.10    echo "    -R           open ROOT entry of logic session and use its parent"
    3.11 @@ -134,7 +133,6 @@
    3.12  
    3.13  # options
    3.14  
    3.15 -JEDIT_ALL_KNOWN=""
    3.16  BUILD_ONLY=false
    3.17  BUILD_JARS="jars"
    3.18  ML_PROCESS_POLICY=""
    3.19 @@ -147,12 +145,9 @@
    3.20  function getoptions()
    3.21  {
    3.22    OPTIND=1
    3.23 -  while getopts "AD:J:Rbd:fj:l:m:np:s" OPT
    3.24 +  while getopts "D:J:Rbd:fj:l:m:np:s" OPT
    3.25    do
    3.26      case "$OPT" in
    3.27 -      A)
    3.28 -        JEDIT_ALL_KNOWN="true"
    3.29 -        ;;
    3.30        D)
    3.31          JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
    3.32          ;;
    3.33 @@ -376,7 +371,7 @@
    3.34  
    3.35  if [ "$BUILD_ONLY" = false ]
    3.36  then
    3.37 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_ALL_KNOWN JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.38 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.39    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    3.40    classpath "$JEDIT_HOME/dist/jedit.jar"
    3.41    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Apr 21 18:51:24 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 21 18:57:30 2017 +0200
     4.3 @@ -74,9 +74,8 @@
     4.4      val session_name = JEdit_Sessions.session_name(options)
     4.5      val session_base =
     4.6        try {
     4.7 -        Sessions.session_base(options, session_name,
     4.8 -          dirs = JEdit_Sessions.session_dirs(),
     4.9 -          all_known = Isabelle_System.getenv("JEDIT_ALL_KNOWN") == "true")
    4.10 +        Sessions.session_base(
    4.11 +          options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
    4.12        }
    4.13        catch { case ERROR(_) => Sessions.Base.pure(options) }
    4.14