optionally explore all sessions -- potentially slow, e.g. for AFP;
--- a/NEWS Wed Apr 19 16:22:20 2017 +0200
+++ b/NEWS Wed Apr 19 16:24:59 2017 +0200
@@ -56,6 +56,9 @@
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 Wed Apr 19 16:22:20 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy Wed Apr 19 16:24:59 2017 +0200
@@ -231,6 +231,7 @@
\<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
@@ -257,6 +258,11 @@
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 Wed Apr 19 16:22:20 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Apr 19 16:24:59 2017 +0200
@@ -97,6 +97,7 @@
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"
@@ -133,6 +134,7 @@
# options
+JEDIT_ALL_KNOWN=""
BUILD_ONLY=false
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
@@ -145,9 +147,12 @@
function getoptions()
{
OPTIND=1
- while getopts "D:J:Rbd:fj:l:m:np:s" OPT
+ while getopts "AD:J:Rbd:fj:l:m:np:s" OPT
do
case "$OPT" in
+ A)
+ JEDIT_ALL_KNOWN="true"
+ ;;
D)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
;;
@@ -371,7 +376,7 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_ALL_KNOWN 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 Wed Apr 19 16:22:20 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Apr 19 16:24:59 2017 +0200
@@ -73,7 +73,11 @@
val options = this.options.value
val session_name = JEdit_Sessions.session_name(options)
val session_base =
- try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
+ try {
+ Sessions.session_base(options, session_name,
+ dirs = JEdit_Sessions.session_dirs(),
+ all_known = Isabelle_System.getenv("JEDIT_ALL_KNOWN") == "true")
+ }
catch { case ERROR(_) => Sessions.Base.pure(options) }
_resources = new JEdit_Resources(session_base.platform_path)