clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;
authorwenzelm
Mon Apr 24 11:23:07 2017 +0200 (2017-04-24)
changeset 655726acb28e5ba41
parent 65571 923e32ad0976
child 65573 0f3fdf689bf9
clarified meaning of "isabelle jedit -R": avoid potential problems with all_known = true;
NEWS
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/NEWS	Mon Apr 24 11:05:24 2017 +0200
     1.2 +++ b/NEWS	Mon Apr 24 11:23:07 2017 +0200
     1.3 @@ -52,9 +52,10 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 -* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
     1.8 -entry of the specified logic session in the editor, while its parent is
     1.9 -used for formal checking.
    1.10 +* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
    1.11 +image of the SESSION, with qualified theory imports restricted to that
    1.12 +portion of the session graph. Moreover, the ROOT entry of the SESSION is
    1.13 +opened in the editor.
    1.14  
    1.15  * The PIDE document model maintains file content independently of the
    1.16  status of jEdit editor buffers. Reloading jEdit buffers no longer causes
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Mon Apr 24 11:05:24 2017 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Apr 24 11:23:07 2017 +0200
     2.3 @@ -233,7 +233,7 @@
     2.4    Options are:
     2.5      -D NAME=X    set JVM system property
     2.6      -J OPTION    add JVM runtime option
     2.7 -    -R           open ROOT entry of logic session and use its parent
     2.8 +    -R           restrict to parent of logic session and open its ROOT
     2.9      -b           build only
    2.10      -d DIR       include session directory
    2.11      -f           fresh build
    2.12 @@ -257,10 +257,12 @@
    2.13    The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
    2.14    session image.
    2.15  
    2.16 -  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    2.17 -  entry of the specified session is opened in the editor, while its parent
    2.18 -  session is used for formal checking. This facilitates maintenance of a
    2.19 -  broken session, by moving the Prover IDE quickly to relevant source files.
    2.20 +  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close>~\<open>session\<close> as follows: the
    2.21 +  parent image of the \<open>session\<close> is used, with qualified theory imports
    2.22 +  restricted to that portion of the session graph. Moreover, the \<^verbatim>\<open>ROOT\<close> entry
    2.23 +  of the \<open>session\<close> is opened in the editor. This facilitates maintenance of a
    2.24 +  particular session, by moving the Prover IDE quickly to relevant source
    2.25 +  files.
    2.26  
    2.27    The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
    2.28    Note that the system option @{system_option_ref jedit_print_mode} allows to
     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Apr 24 11:05:24 2017 +0200
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Apr 24 11:23:07 2017 +0200
     3.3 @@ -99,7 +99,7 @@
     3.4    echo "  Options are:"
     3.5    echo "    -D NAME=X    set JVM system property"
     3.6    echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
     3.7 -  echo "    -R           open ROOT entry of logic session and use its parent"
     3.8 +  echo "    -R           restrict to parent of logic session and open its ROOT"
     3.9    echo "    -b           build only"
    3.10    echo "    -d DIR       include session directory"
    3.11    echo "    -f           fresh build"
    3.12 @@ -137,7 +137,7 @@
    3.13  BUILD_JARS="jars"
    3.14  ML_PROCESS_POLICY=""
    3.15  JEDIT_SESSION_DIRS=""
    3.16 -JEDIT_LOGIC_ROOT=""
    3.17 +JEDIT_LOGIC_RESTRICT=""
    3.18  JEDIT_LOGIC=""
    3.19  JEDIT_PRINT_MODE=""
    3.20  JEDIT_BUILD_MODE="normal"
    3.21 @@ -155,7 +155,7 @@
    3.22          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    3.23          ;;
    3.24        R)
    3.25 -        JEDIT_LOGIC_ROOT="true"
    3.26 +        JEDIT_LOGIC_RESTRICT="true"
    3.27          ;;
    3.28        b)
    3.29          BUILD_ONLY=true
    3.30 @@ -371,7 +371,7 @@
    3.31  
    3.32  if [ "$BUILD_ONLY" = false ]
    3.33  then
    3.34 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.35 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.36    export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
    3.37    classpath "$JEDIT_HOME/dist/jedit.jar"
    3.38    exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
     4.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:05:24 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:23:07 2017 +0200
     4.3 @@ -30,6 +30,9 @@
     4.4        case s => options.string("ML_process_policy") = s
     4.5      }
     4.6  
     4.7 +  def session_restricted(): Boolean =
     4.8 +    Isabelle_System.getenv("JEDIT_LOGIC_RESTRICT") == "true"
     4.9 +
    4.10    def session_info(options: Options): Info =
    4.11    {
    4.12      val logic =
    4.13 @@ -43,16 +46,19 @@
    4.14          catch { case ERROR(_) => None }
    4.15        info <- sessions.get(logic)
    4.16        parent <- info.parent
    4.17 -      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
    4.18 +      if session_restricted()
    4.19      } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
    4.20    }
    4.21  
    4.22    def session_name(options: Options): String = session_info(options).name
    4.23  
    4.24    def session_base(options: Options): Sessions.Base =
    4.25 +  {
    4.26 +    val all_known = !session_restricted()
    4.27      Sessions.session_base(
    4.28 -      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    4.29 +      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
    4.30      .platform_path
    4.31 +  }
    4.32  
    4.33    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    4.34