--- a/NEWS Thu Aug 31 17:21:38 2017 +0200
+++ b/NEWS Thu Aug 31 17:31:56 2017 +0200
@@ -100,10 +100,9 @@
* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.
-* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
-image of the SESSION, with qualified theory imports restricted to that
-portion of the session graph. Moreover, the ROOT entry of the SESSION is
-opened in the editor.
+* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
+entry of the specified logic session in the editor, while its parent is
+used for formal checking.
* The main Isabelle/jEdit plugin may be restarted manually (using the
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
--- a/src/Doc/JEdit/JEdit.thy Thu Aug 31 17:21:38 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Aug 31 17:31:56 2017 +0200
@@ -232,7 +232,7 @@
Options are:
-D NAME=X set JVM system property
-J OPTION add JVM runtime option
- -R restrict to parent of logic session and open its ROOT
+ -R open ROOT entry of logic session and use its parent
-b build only
-d DIR include session directory
-f fresh build
@@ -256,12 +256,10 @@
The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
session image.
- Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close>~\<open>session\<close> as follows: the
- parent image of the \<open>session\<close> is used, with qualified theory imports
- restricted to that portion of the session graph. Moreover, the \<^verbatim>\<open>ROOT\<close> entry
- of the \<open>session\<close> is opened in the editor. This facilitates maintenance of a
- particular session, by moving the Prover IDE quickly to relevant source
- files.
+ 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
+ broken session, by moving the Prover IDE quickly to relevant source files.
The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
Note that the system option @{system_option_ref jedit_print_mode} allows to
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Aug 31 17:21:38 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Aug 31 17:31:56 2017 +0200
@@ -110,7 +110,7 @@
echo " Options are:"
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 restrict to parent of logic session and open its ROOT"
+ echo " -R open ROOT entry of logic session and use its parent"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
@@ -148,7 +148,7 @@
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
JEDIT_SESSION_DIRS=""
-JEDIT_LOGIC_RESTRICT=""
+JEDIT_LOGIC_ROOT=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_BUILD_MODE="normal"
@@ -166,7 +166,7 @@
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
;;
R)
- JEDIT_LOGIC_RESTRICT="true"
+ JEDIT_LOGIC_ROOT="true"
;;
b)
BUILD_ONLY=true
@@ -408,7 +408,7 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT 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/jedit_sessions.scala Thu Aug 31 17:21:38 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Aug 31 17:31:56 2017 +0200
@@ -30,9 +30,6 @@
case s => options.string("ML_process_policy") = s
}
- def session_restricted(): Boolean =
- Isabelle_System.getenv("JEDIT_LOGIC_RESTRICT") == "true"
-
def session_info(options: Options): Info =
{
val logic =
@@ -46,7 +43,7 @@
catch { case ERROR(_) => None }
info <- sessions.get(logic)
parent <- info.parent
- if session_restricted()
+ if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
} yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
}
@@ -54,10 +51,9 @@
def session_base(options: Options): (List[String], Sessions.Base) =
{
- val all_known = !session_restricted()
val (errs, base) =
Sessions.session_base_errors(
- options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
+ options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
(errs, base.platform_path)
}