--- 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
--- 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
--- 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 */
--- 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 }
--- 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")" \
--- 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))
}