# HG changeset patch
# User wenzelm
# Date 1344937078 -7200
# Node ID 9e8f30bfbdcac59a4f21db690785cec25c5e3935
# Parent  6e739225dd8a619c04bb9a37a31e3a9804d4e7c6
added jedit option -d;

diff -r 6e739225dd8a -r 9e8f30bfbdca doc-src/System/Thy/Interfaces.thy
--- a/doc-src/System/Thy/Interfaces.thy	Tue Aug 14 10:44:03 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy	Tue Aug 14 11:37:58 2012 +0200
@@ -15,6 +15,7 @@
   Options are:
     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     -b           build only
+    -d DIR       include session directory
     -f           fresh build
     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
     -l NAME      logic image name (default ISABELLE_LOGIC)
@@ -24,8 +25,12 @@
 (default Scratch.thy).
 \end{ttbox}
 
-  The @{verbatim "-l"} option specifies the logic image.  The
-  @{verbatim "-m"} option specifies additional print modes.
+  The @{verbatim "-l"} option specifies the session name of the logic
+  image to be used for proof processing.  Additional session root
+  directories may be included via option @{verbatim "-d"} to augment
+  that name space (see also \secref{sec:tool-build}).
+
+  The @{verbatim "-m"} option specifies additional print modes.
 
   The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
   additional low-level options to the JVM or jEdit, respectively.  The
diff -r 6e739225dd8a -r 9e8f30bfbdca doc-src/System/Thy/document/Interfaces.tex
--- a/doc-src/System/Thy/document/Interfaces.tex	Tue Aug 14 10:44:03 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex	Tue Aug 14 11:37:58 2012 +0200
@@ -36,6 +36,7 @@
   Options are:
     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     -b           build only
+    -d DIR       include session directory
     -f           fresh build
     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
     -l NAME      logic image name (default ISABELLE_LOGIC)
@@ -45,8 +46,12 @@
 (default Scratch.thy).
 \end{ttbox}
 
-  The \verb|-l| option specifies the logic image.  The
-  \verb|-m| option specifies additional print modes.
+  The \verb|-l| option specifies the session name of the logic
+  image to be used for proof processing.  Additional session root
+  directories may be included via option \verb|-d| to augment
+  that name space (see also \secref{sec:tool-build}).
+
+  The \verb|-m| option specifies additional print modes.
 
   The \verb|-J| and \verb|-j| options allow to pass
   additional low-level options to the JVM or jEdit, respectively.  The
diff -r 6e739225dd8a -r 9e8f30bfbdca src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Aug 14 10:44:03 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 14 11:37:58 2012 +0200
@@ -366,13 +366,14 @@
           deps + (name -> Session_Content(loaded_theories, syntax, sources))
       }))
 
-  def session_content(session: String): Session_Content =
+  def session_content(dirs: List[Path], session: String): Session_Content =
   {
-    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
+    val (_, tree) =
+      find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
     dependencies(false, tree)(session)
   }
 
-  def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
+  def outer_syntax(session: String): Outer_Syntax = session_content(Nil, session).syntax
 
 
   /* jobs */
diff -r 6e739225dd8a -r 9e8f30bfbdca src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 14 10:44:03 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 14 11:37:58 2012 +0200
@@ -171,7 +171,7 @@
 
   /* actor messages */
 
-  private case class Start(logic: String, args: List[String])
+  private case class Start(dirs: List[Path], logic: String, args: List[String])
   private case object Cancel_Execution
   private case class Edit(edits: List[Document.Edit_Text])
   private case class Change(
@@ -377,12 +377,12 @@
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(name, args) if prover.isEmpty =>
+        case Start(dirs, name, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
 
             // FIXME static init in main constructor
-            val content = Build.session_content(name)
+            val content = Build.session_content(dirs, name)
             thy_load.register_thys(content.loaded_theories)
             base_syntax = content.syntax
 
@@ -440,7 +440,8 @@
 
   /* actions */
 
-  def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
+  def start(dirs: List[Path], name: String, args: List[String])
+  { session_actor ! Start(dirs, name, args) }
 
   def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
 
diff -r 6e739225dd8a -r 9e8f30bfbdca src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 14 10:44:03 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 14 11:37:58 2012 +0200
@@ -52,6 +52,7 @@
   echo "    -J OPTION    add JVM runtime option"
   echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
   echo "    -b           build only"
+  echo "    -d DIR       include session directory"
   echo "    -f           fresh build"
   echo "    -j OPTION    add jEdit runtime option"
   echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
@@ -82,13 +83,14 @@
 
 BUILD_ONLY=false
 BUILD_JARS="jars"
+JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC="$ISABELLE_LOGIC"
 JEDIT_PRINT_MODE=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "J:bdfj:l:m:" OPT
+  while getopts "J:bd:fj:l:m:" OPT
   do
     case "$OPT" in
       J)
@@ -97,6 +99,13 @@
       b)
         BUILD_ONLY=true
         ;;
+      d)
+        if [ -z "$JEDIT_SESSION_DIRS" ]; then
+          JEDIT_SESSION_DIRS="$OPTARG"
+        else
+          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
+        fi
+        ;;
       f)
         BUILD_JARS="jars_fresh"
         ;;
@@ -283,7 +292,7 @@
       ;;
   esac
 
-  export JEDIT_LOGIC JEDIT_PRINT_MODE
+  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
 
   exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
     -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
diff -r 6e739225dd8a -r 9e8f30bfbdca src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 14 10:44:03 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 14 11:37:58 2012 +0200
@@ -300,6 +300,7 @@
 
   def start_session()
   {
+    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     val logic = {
       val logic = Property("logic")
@@ -307,7 +308,7 @@
       else Isabelle.default_logic()
     }
     val name = Path.explode(logic).base.implode  // FIXME more robust session name
-    session.start(name, modes ::: List(logic))
+    session.start(dirs, name, modes ::: List(logic))
   }