--- a/NEWS Thu Nov 02 10:16:22 2017 +0100
+++ b/NEWS Thu Nov 02 11:25:37 2017 +0100
@@ -34,14 +34,18 @@
* Completion supports theory header imports.
-* 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
+* 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
+ Example: isabelle jedit -A HOL -S Formal_SSA -d '$AFP'
+
*** HOL ***
--- a/src/Doc/JEdit/JEdit.thy Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Nov 02 11:25:37 2017 +0100
@@ -228,6 +228,7 @@
\<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
-D NAME=X set JVM system property
@@ -260,15 +261,14 @@
The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
session image.
- Option \<^verbatim>\<open>-B\<close> and \<^verbatim>\<open>-P\<close> are mutually exclusive and modify the meaning of
- option \<^verbatim>\<open>-l\<close> as follows: \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on
- the required theory imports from other sessions, or the parent session image
- if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
- session image directly.
+ 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>-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>-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
--- a/src/Pure/Thy/sessions.scala Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Nov 02 11:25:37 2017 +0100
@@ -152,6 +152,7 @@
{
def is_empty: Boolean = session_bases.isEmpty
def apply(name: String): Base = session_bases(name)
+ def get(name: String): Option[Base] = session_bases.get(name)
def imported_sources(name: String): List[SHA1.Digest] =
session_bases(name).imported_sources.map(_._2)
@@ -337,6 +338,7 @@
def base_info(options: Options, session: String,
dirs: List[Path] = Nil,
+ ancestor_session: Option[String] = None,
all_known: Boolean = false,
focus_session: Boolean = false,
required_session: Boolean = false): Base_Info =
@@ -346,24 +348,30 @@
val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
val info = selected_sessions(session)
+ val ancestor = ancestor_session orElse info.parent
val (session1, infos1) =
- if (required_session && info.parent.isDefined) {
+ if (required_session && ancestor.isDefined) {
val deps = Sessions.deps(selected_sessions, global_theories)
val base = deps(session)
- val parent_loaded = deps(info.parent.get).loaded_theories.defined(_)
+ val ancestor_loaded =
+ deps.get(ancestor.get) match {
+ case None =>
+ error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
+ case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_)
+ }
val required_theories =
for {
thy <- base.loaded_theories.keys
- if !parent_loaded(thy) && base.theory_qualifier(thy) != session
+ if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
}
yield thy
- if (required_theories.isEmpty) (info.parent.get, Nil)
+ if (required_theories.isEmpty) (ancestor.get, Nil)
else {
- val other_name = info.name + "(base)"
+ val other_name = info.name + "_base(" + ancestor.get + ")"
(other_name,
List(
make_info(info.options,
@@ -375,7 +383,7 @@
name = other_name,
groups = info.groups,
path = ".",
- parent = info.parent,
+ parent = ancestor,
description = "Required theory imports from other sessions",
options = Nil,
imports = info.imports,
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Nov 02 11:25:37 2017 +0100
@@ -97,6 +97,7 @@
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 " -D NAME=X set JVM system property"
@@ -141,6 +142,7 @@
BUILD_ONLY=false
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
+JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_BASE=""
JEDIT_LOGIC_FOCUS=""
JEDIT_SESSION_DIRS=""
@@ -153,9 +155,12 @@
function getoptions()
{
OPTIND=1
- while getopts "BFD:J:PRS:bd:fj:l:m:np:s" OPT
+ while getopts "A:BFD:J:PRS:bd:fj:l:m:np:s" OPT
do
case "$OPT" in
+ A)
+ JEDIT_LOGIC_ANCESTOR="$OPTARG"
+ ;;
B)
JEDIT_LOGIC_BASE="true"
JEDIT_LOGIC_PARENT=""
@@ -424,7 +429,7 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_BASE JEDIT_LOGIC_FOCUS \
+ 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_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
--- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 02 10:16:22 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 02 11:25:37 2017 +0100
@@ -39,6 +39,7 @@
Isabelle_System.getenv("JEDIT_LOGIC"),
options.string(jedit_logic_option))
+ def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
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"
@@ -109,6 +110,7 @@
if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
else logic_name(options),
dirs = JEdit_Sessions.session_dirs(),
+ ancestor_session = logic_ancestor,
all_known = !logic_focus,
focus_session = logic_focus,
required_session = logic_base)