--- a/NEWS Sun Jun 03 23:30:53 2018 +0200
+++ b/NEWS Mon Jun 04 14:21:16 2018 +0200
@@ -89,16 +89,16 @@
E.g. "Prob" may be completed to "HOL-Probability.Probability".
* The command-line tool "isabelle jedit" provides more flexible options
-for session selection:
- - options -P opens the parent session image of -l
- - options -A and -B modify the meaning of -l to produce a base
- image on the spot, based on the specified ancestor (or parent)
- - 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
+for session management:
+ - option -R builds an auxiliary logic image with all required theories
+ from other sessions, relative to an ancestor session given by option
+ -A (default: parent)
+ - option -S is like -R, with a focus on the selected session and its
+ descendants (this reduces startup time for big projects like AFP)
Examples:
+ isabelle jedit -R HOL-Number_Theory
+ isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
--- a/src/Doc/JEdit/JEdit.thy Sun Jun 03 23:30:53 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy Mon Jun 04 14:21:16 2018 +0200
@@ -228,15 +228,12 @@
\<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
Options are:
- -A specify ancestor for base session image (default: parent)
- -B use base session image, with theories from other sessions
- -F focus on selected logic session: ignore unrelated theories
+ -A NAME ancestor session for options -R and -S (default: parent)
-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, abbreviates -B -F -R -l NAME
+ -R NAME build image with requirements from other sessions
+ -S NAME like option -R, with focus on selected session
-b build only
-d DIR include session directory
-f fresh build
@@ -261,18 +258,15 @@
The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
session image.
- Option \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-B\<close> and are mutually exclusive and modify the meaning of
- option \<^verbatim>\<open>-l\<close> as follows. Option \<^verbatim>\<open>-P\<close> opens the parent session image. Option
- \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on the required theory
- imports from other sessions, relative to an ancestor session given by option
- \<^verbatim>\<open>-A\<close> (default: parent session).
+ Option \<^verbatim>\<open>-R\<close> builds an auxiliary logic image with all required theories from
+ \<^emph>\<open>other\<close> sessions, relative to an ancestor session given by option \<^verbatim>\<open>-A\<close>
+ (default: parent session). Option \<^verbatim>\<open>-R\<close> also opens the session \<^verbatim>\<open>ROOT\<close> entry
+ in the editor, to facilitate editing of the main session.
- Option \<^verbatim>\<open>-F\<close> focuses on the effective logic session: the accessible
- namespace of theories is restricted to sessions that are connected to it.
-
- 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>.
+ Option \<^verbatim>\<open>-S\<close> is like \<^verbatim>\<open>-R\<close>, with a focus on the selected session and its
+ descendants: the namespace of accessible theories is restricted accordingly.
+ This reduces startup time for big projects, notably the ``Archive of Formal
+ Proofs''.
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/Pure/Thy/sessions.scala Sun Jun 03 23:30:53 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Jun 04 14:21:16 2018 +0200
@@ -394,21 +394,21 @@
progress: Progress = No_Progress,
dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
- ancestor_session: Option[String] = None,
- all_known: Boolean = false,
- focus_session: Boolean = false,
- required_session: Boolean = false): Base_Info =
+ session_ancestor: Option[String] = None,
+ session_requirements: Boolean = false,
+ session_focus: Boolean = false,
+ all_known: Boolean = false): Base_Info =
{
val full_sessions = load_structure(options, dirs = dirs)
val global_theories = full_sessions.global_theories
val selected_sessions =
- full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))
+ full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
val info = selected_sessions(session)
- val ancestor = ancestor_session orElse info.parent
+ val ancestor = session_ancestor orElse info.parent
val (session1, infos1) =
- if (required_session && ancestor.isDefined) {
+ if (session_requirements && ancestor.isDefined) {
val deps = Sessions.deps(selected_sessions, global_theories, progress = progress)
val base = deps(session)
@@ -430,7 +430,7 @@
if (required_theories.isEmpty) (ancestor.get, Nil)
else {
- val other_name = info.name + "_base(" + ancestor.get + ")"
+ val other_name = info.name + "_requirements(" + ancestor.get + ")"
(other_name,
List(
make_info(info.options,
@@ -461,7 +461,7 @@
{
val sel_sessions1 = session1 :: include_sessions
val select_sessions1 =
- if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
+ if (session_focus) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
full_sessions1.selection(Selection(sessions = select_sessions1))
}
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Jun 03 23:30:53 2018 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jun 04 14:21:16 2018 +0200
@@ -97,15 +97,12 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
echo
echo " Options are:"
- echo " -A specify ancestor for base session image (default: parent)"
- echo " -B use base session image, with theories from other sessions"
- echo " -F focus on selected logic session: ignore unrelated theories"
+ echo " -A NAME ancestor session for options -R and -S (default: parent)"
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, abbreviates -B -F -R -l NAME"
+ echo " -R NAME build image with requirements from other sessions"
+ echo " -S NAME like option -R, with focus on selected session"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
@@ -143,11 +140,9 @@
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
-JEDIT_LOGIC_BASE=""
+JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_LOGIC_FOCUS=""
JEDIT_SESSION_DIRS=""
-JEDIT_LOGIC_ROOT=""
-JEDIT_LOGIC_PARENT=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_BUILD_MODE="normal"
@@ -155,38 +150,26 @@
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
+ while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
do
case "$OPT" in
A)
JEDIT_LOGIC_ANCESTOR="$OPTARG"
;;
- B)
- JEDIT_LOGIC_BASE="true"
- JEDIT_LOGIC_PARENT=""
- ;;
D)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
;;
- F)
- JEDIT_LOGIC_FOCUS="true"
- ;;
J)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
;;
- P)
- JEDIT_LOGIC_PARENT="true"
- JEDIT_LOGIC_BASE=""
- ;;
R)
- JEDIT_LOGIC_ROOT="true"
+ JEDIT_LOGIC="$OPTARG"
+ JEDIT_LOGIC_REQUIREMENTS="true"
;;
S)
JEDIT_LOGIC="$OPTARG"
- JEDIT_LOGIC_BASE="true"
- JEDIT_LOGIC_PARENT=""
+ JEDIT_LOGIC_REQUIREMENTS="true"
JEDIT_LOGIC_FOCUS="true"
- JEDIT_LOGIC_ROOT="true"
;;
b)
BUILD_ONLY=true
@@ -429,8 +412,8 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
- JEDIT_LOGIC_PARENT JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
+ JEDIT_LOGIC_FOCUS 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 Sun Jun 03 23:30:53 2018 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Mon Jun 04 14:21:16 2018 +0200
@@ -40,9 +40,8 @@
options.string(jedit_logic_option))
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
+ def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
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"
def logic_info(options: Options): Option[Sessions.Info] =
try {
@@ -52,9 +51,7 @@
catch { case ERROR(_) => None }
def logic_root(options: Options): Position.T =
- if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
- logic_info(options).map(_.pos) getOrElse Position.none
- }
+ if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
else Position.none
@@ -111,13 +108,11 @@
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
dirs = JEdit_Sessions.session_dirs(),
- session =
- if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
- else logic_name(options),
- ancestor_session = logic_ancestor,
- all_known = !logic_focus,
- focus_session = logic_focus,
- required_session = logic_base)
+ session = logic_name(options),
+ session_ancestor = logic_ancestor,
+ session_requirements = logic_requirements,
+ session_focus = logic_focus,
+ all_known = !logic_focus)
def session_build(
options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =