# HG changeset patch
# User wenzelm
# Date 1530283554 -7200
# Node ID 12b4b3bc585d8ede473db256a2dc0d7bb921306e
# Parent  000a0e062529b3de3a6c0dff0e0ddce60c847fa9
command-line option for include_sessions;

diff -r 000a0e062529 -r 12b4b3bc585d NEWS
--- 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.
diff -r 000a0e062529 -r 12b4b3bc585d src/Doc/JEdit/JEdit.thy
--- 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
diff -r 000a0e062529 -r 12b4b3bc585d src/Doc/System/Environment.thy
--- 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.
 
diff -r 000a0e062529 -r 12b4b3bc585d src/Pure/ML/ml_console.scala
--- 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") {
diff -r 000a0e062529 -r 12b4b3bc585d src/Tools/jEdit/lib/Tools/jedit
--- 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[@]}"
diff -r 000a0e062529 -r 12b4b3bc585d src/Tools/jEdit/src/jedit_sessions.scala
--- 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,