--- a/NEWS Fri Jun 29 15:54:41 2018 +0200
+++ b/NEWS Fri Jun 29 16:45:54 2018 +0200
@@ -85,11 +85,15 @@
- option -A specifies an alternative ancestor session for options -R
and -S
+ - option -i includes additional sessions into the name-space of
+ theories
+
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
+ isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
* PIDE markup for session ROOT files: allows to complete session names,
follow links to theories and document files etc.
--- a/src/Doc/JEdit/JEdit.thy Fri Jun 29 15:54:41 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri Jun 29 16:45:54 2018 +0200
@@ -237,6 +237,7 @@
-b build only
-d DIR include session directory
-f fresh build
+ -i NAME include session in name-space of theories
-j OPTION add jEdit runtime option
(default $JEDIT_OPTIONS)
-l NAME logic image name
@@ -266,6 +267,9 @@
ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
hierarchy of session images on the spot.
+ The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
+ theories: multiple occurrences are possible.
+
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
--- a/src/Doc/System/Environment.thy Fri Jun 29 15:54:41 2018 +0200
+++ b/src/Doc/System/Environment.thy Fri Jun 29 16:45:54 2018 +0200
@@ -407,6 +407,7 @@
Options are:
-d DIR include session directory
+ -i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC)
-m MODE add print mode for output
-n no build of session image on startup
@@ -421,6 +422,9 @@
Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+ Option \<^verbatim>\<open>-i\<close> includes additional sessions into the name-space of theories:
+ multiple occurrences are possible.
+
Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
relevant for Isabelle/Pure development.
--- a/src/Pure/ML/ml_console.scala Fri Jun 29 15:54:41 2018 +0200
+++ b/src/Pure/ML/ml_console.scala Fri Jun 29 16:45:54 2018 +0200
@@ -15,6 +15,7 @@
{
Command_Line.tool {
var dirs: List[Path] = Nil
+ var include_sessions: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var modes: List[String] = Nil
var no_build = false
@@ -27,6 +28,7 @@
Options are:
-d DIR include session directory
+ -i NAME include session in name-space of theories
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-m MODE add print mode for output
-n no build of session image on startup
@@ -39,6 +41,7 @@
quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """.
""",
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "i:" -> (arg => include_sessions = include_sessions ::: List(arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"n" -> (arg => no_build = true),
@@ -69,7 +72,8 @@
store = Some(Sessions.store(options, system_mode)),
session_base =
if (raw_ml_system) None
- else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
+ else Some(Sessions.base_info(
+ options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
val process_result = Future.thread[Int]("process_result") {
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jun 29 15:54:41 2018 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jun 29 16:45:54 2018 +0200
@@ -106,6 +106,7 @@
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
+ echo " -i NAME include session in name-space of theories"
echo " -j OPTION add jEdit runtime option"
echo " (default $JEDIT_OPTIONS)"
echo " -l NAME logic session name"
@@ -142,6 +143,7 @@
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_LOGIC_FOCUS=""
+JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
@@ -150,7 +152,7 @@
function getoptions()
{
OPTIND=1
- while getopts "A:BFD:J:R:S:bd:fj:l:m:np:s" OPT
+ while getopts "A:BFD:J:R:S:bd:fi:j:l:m:np:s" OPT
do
case "$OPT" in
A)
@@ -181,6 +183,13 @@
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
fi
;;
+ i)
+ if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
+ JEDIT_INCLUDE_SESSIONS="$OPTARG"
+ else
+ JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
+ fi
+ ;;
f)
BUILD_JARS="jars_fresh"
;;
@@ -413,7 +422,7 @@
if [ "$BUILD_ONLY" = false ]
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
- JEDIT_LOGIC_FOCUS JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ JEDIT_LOGIC_FOCUS JEDIT_INCLUDE_SESSIONS 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 Fri Jun 29 15:54:41 2018 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Jun 29 16:45:54 2018 +0200
@@ -42,6 +42,8 @@
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_include_sessions: List[String] =
+ space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
def logic_info(options: Options): Option[Sessions.Info] =
try {
@@ -108,6 +110,7 @@
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
dirs = JEdit_Sessions.session_dirs(),
+ include_sessions = logic_include_sessions,
session = logic_name(options),
session_ancestor = logic_ancestor,
session_requirements = logic_requirements,