reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
authorwenzelm
Thu Aug 31 17:31:56 2017 +0200 (21 months ago)
changeset 66574e16b27bd3f76
parent 66573 a6401a6417cf
child 66575 191048506504
reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
NEWS
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/NEWS	Thu Aug 31 17:21:38 2017 +0200
     1.2 +++ b/NEWS	Thu Aug 31 17:31:56 2017 +0200
     1.3 @@ -100,10 +100,9 @@
     1.4  * Action "isabelle.preview" opens an HTML preview of the current theory
     1.5  document in the default web browser.
     1.6  
     1.7 -* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
     1.8 -image of the SESSION, with qualified theory imports restricted to that
     1.9 -portion of the session graph. Moreover, the ROOT entry of the SESSION is
    1.10 -opened in the editor.
    1.11 +* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
    1.12 +entry of the specified logic session in the editor, while its parent is
    1.13 +used for formal checking.
    1.14  
    1.15  * The main Isabelle/jEdit plugin may be restarted manually (using the
    1.16  jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Aug 31 17:21:38 2017 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Aug 31 17:31:56 2017 +0200
     2.3 @@ -232,7 +232,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           restrict to parent of logic session and open its ROOT
     2.8 +    -R           open ROOT entry of logic session and use its parent
     2.9      -b           build only
    2.10      -d DIR       include session directory
    2.11      -f           fresh build
    2.12 @@ -256,12 +256,10 @@
    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>~\<open>session\<close> as follows: the
    2.17 -  parent image of the \<open>session\<close> is used, with qualified theory imports
    2.18 -  restricted to that portion of the session graph. Moreover, the \<^verbatim>\<open>ROOT\<close> entry
    2.19 -  of the \<open>session\<close> is opened in the editor. This facilitates maintenance of a
    2.20 -  particular session, by moving the Prover IDE quickly to relevant source
    2.21 -  files.
    2.22 +  Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
    2.23 +  entry of the specified session is opened in the editor, while its parent
    2.24 +  session is used for formal checking. This facilitates maintenance of a
    2.25 +  broken session, by moving the Prover IDE quickly to relevant source 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	Thu Aug 31 17:21:38 2017 +0200
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Aug 31 17:31:56 2017 +0200
     3.3 @@ -110,7 +110,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           restrict to parent of logic session and open its ROOT"
     3.8 +  echo "    -R           open ROOT entry of logic session and use its parent"
     3.9    echo "    -b           build only"
    3.10    echo "    -d DIR       include session directory"
    3.11    echo "    -f           fresh build"
    3.12 @@ -148,7 +148,7 @@
    3.13  BUILD_JARS="jars"
    3.14  ML_PROCESS_POLICY=""
    3.15  JEDIT_SESSION_DIRS=""
    3.16 -JEDIT_LOGIC_RESTRICT=""
    3.17 +JEDIT_LOGIC_ROOT=""
    3.18  JEDIT_LOGIC=""
    3.19  JEDIT_PRINT_MODE=""
    3.20  JEDIT_BUILD_MODE="normal"
    3.21 @@ -166,7 +166,7 @@
    3.22          JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
    3.23          ;;
    3.24        R)
    3.25 -        JEDIT_LOGIC_RESTRICT="true"
    3.26 +        JEDIT_LOGIC_ROOT="true"
    3.27          ;;
    3.28        b)
    3.29          BUILD_ONLY=true
    3.30 @@ -408,7 +408,7 @@
    3.31  
    3.32  if [ "$BUILD_ONLY" = false ]
    3.33  then
    3.34 -  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
    3.35 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT 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	Thu Aug 31 17:21:38 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Aug 31 17:31:56 2017 +0200
     4.3 @@ -30,9 +30,6 @@
     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 @@ -46,7 +43,7 @@
    4.14          catch { case ERROR(_) => None }
    4.15        info <- sessions.get(logic)
    4.16        parent <- info.parent
    4.17 -      if session_restricted()
    4.18 +      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
    4.19      } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
    4.20    }
    4.21  
    4.22 @@ -54,10 +51,9 @@
    4.23  
    4.24    def session_base(options: Options): (List[String], Sessions.Base) =
    4.25    {
    4.26 -    val all_known = !session_restricted()
    4.27      val (errs, base) =
    4.28        Sessions.session_base_errors(
    4.29 -        options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
    4.30 +        options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    4.31      (errs, base.platform_path)
    4.32    }
    4.33