support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
--- a/NEWS Wed Nov 01 22:13:38 2017 +0100
+++ b/NEWS Thu Nov 02 10:16:22 2017 +0100
@@ -34,9 +34,13 @@
* Completion supports theory header imports.
-* The "isabelle jedit" command-line options -B or -P modify the meaning
-of -l to produce an image on the spot or use the session parent image.
-Option -R now only opens the session ROOT entry.
+* The command-line tool "isabelle jedit" provides more flexible options:
+ - options -B or -P modify the meaning of -l to produce an image on the
+ spot or use the session parent image
+ - option -F focuses on the specified logic session
+ - option -R has changed: it only opens the session ROOT entry
+ - option -S sets up the development environment to edit the
+ specified session: it abbreviates -B -F -R -l
*** HOL ***
--- a/src/Doc/JEdit/JEdit.thy Wed Nov 01 22:13:38 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Nov 02 10:16:22 2017 +0100
@@ -229,11 +229,13 @@
Options are:
-B use base session image, with theories from other sessions
+ -F focus on selected logic session: ignore unrelated theories
-D NAME=X set JVM system property
-J OPTION add JVM runtime option
(default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
-P use parent session image
-R open ROOT entry of logic session
+ -S NAME edit specified logic session, same as -B -F -R -l NAME
-b build only
-d DIR include session directory
-f fresh build
@@ -264,6 +266,14 @@
if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
session image directly.
+ Option \<^verbatim>\<open>-F\<close> focuses on the specified logic session, as resulting from
+ options \<^verbatim>\<open>-l\<close>, \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-P\<close>. The accessible name space of theories is
+ restricted to sessions that are connected to this session.
+
+ Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
+ editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
+ specified session: it abbreviates \<^verbatim>\<open>-B\<close> \<^verbatim>\<open>-F\<close> \<^verbatim>\<open>-R\<close> \<^verbatim>\<open>-l\<close>.
+
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
do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
@@ -277,9 +287,6 @@
The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
directly to the underlying \<^verbatim>\<open>java\<close> process.
- Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
- editor.
-
The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
Isabelle/jEdit. This is only relevant for building from sources, which also
requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
--- a/src/Pure/Thy/sessions.scala Wed Nov 01 22:13:38 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Nov 02 10:16:22 2017 +0100
@@ -338,6 +338,7 @@
def base_info(options: Options, session: String,
dirs: List[Path] = Nil,
all_known: Boolean = false,
+ focus_session: Boolean = false,
required_session: Boolean = false): Base_Info =
{
val full_sessions = load(options, dirs = dirs)
@@ -387,7 +388,12 @@
val full_sessions1 =
if (infos1.isEmpty) full_sessions
else load(options, dirs = dirs, infos = infos1)
- val selected_sessions1 = full_sessions1.selection(Selection(sessions = List(session1)))._2
+
+ val select_sessions1 =
+ if (focus_session) full_sessions1.imports_descendants(List(session1))
+ else List(session1)
+ val selected_sessions1 =
+ full_sessions1.selection(Selection(sessions = select_sessions1))._2
val sessions1 = if (all_known) full_sessions1 else selected_sessions1
val deps1 = Sessions.deps(sessions1, global_theories)
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Nov 01 22:13:38 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Nov 02 10:16:22 2017 +0100
@@ -98,11 +98,13 @@
echo
echo " Options are:"
echo " -B use base session image, with theories from other sessions"
+ echo " -F focus on selected logic session: ignore unrelated theories"
echo " -D NAME=X set JVM system property"
echo " -J OPTION add JVM runtime option"
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
echo " -P use parent session image"
echo " -R open ROOT entry of logic session"
+ echo " -S NAME edit specified logic session, same as abbreviates -B -F -R -l NAME"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
@@ -140,6 +142,7 @@
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
JEDIT_LOGIC_BASE=""
+JEDIT_LOGIC_FOCUS=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC_ROOT=""
JEDIT_LOGIC_PARENT=""
@@ -150,7 +153,7 @@
function getoptions()
{
OPTIND=1
- while getopts "BD:J:PRbd:fj:l:m:np:s" OPT
+ while getopts "BFD:J:PRS:bd:fj:l:m:np:s" OPT
do
case "$OPT" in
B)
@@ -160,6 +163,9 @@
D)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
;;
+ F)
+ JEDIT_LOGIC_FOCUS="true"
+ ;;
J)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
;;
@@ -170,6 +176,13 @@
R)
JEDIT_LOGIC_ROOT="true"
;;
+ S)
+ JEDIT_LOGIC="$OPTARG"
+ JEDIT_LOGIC_BASE="true"
+ JEDIT_LOGIC_PARENT=""
+ JEDIT_LOGIC_FOCUS="true"
+ JEDIT_LOGIC_ROOT="true"
+ ;;
b)
BUILD_ONLY=true
;;
@@ -411,8 +424,8 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_PARENT \
- JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
+ JEDIT_LOGIC_PARENT 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 Wed Nov 01 22:13:38 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 02 10:16:22 2017 +0100
@@ -39,6 +39,7 @@
Isabelle_System.getenv("JEDIT_LOGIC"),
options.string(jedit_logic_option))
+ def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
@@ -103,15 +104,14 @@
/* session build process */
def session_base_info(options: Options): Sessions.Base_Info =
- {
- val logic = logic_name(options)
-
Sessions.base_info(options,
- if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic,
+ session =
+ if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
+ else logic_name(options),
dirs = JEdit_Sessions.session_dirs(),
- all_known = true,
+ all_known = !logic_focus,
+ focus_session = logic_focus,
required_session = logic_base)
- }
def session_build(
options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =