# HG changeset patch
# User wenzelm
# Date 1458159075 -3600
# Node ID 699e86051e3566786dc93951eaac86889f629fa4
# Parent  751cf9f3d433c718f450b34fcfba61c958343cbf
isabelle process -d;
proper args;

diff -r 751cf9f3d433 -r 699e86051e35 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Mar 16 20:50:38 2016 +0100
+++ b/src/Doc/System/Basics.thy	Wed Mar 16 21:11:15 2016 +0100
@@ -305,6 +305,7 @@
 \<open>Usage: isabelle process [OPTIONS]
 
   Options are:
+    -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
     -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
@@ -324,7 +325,8 @@
   premature exit of the ML process with return code 1.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-l\<close> specifies the logic session name.
+  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
+  additional directories for session roots, see also \secref{sec:tool-build}.
 
   \<^medskip>
   The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
@@ -375,11 +377,11 @@
   abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
   Isabelle/Pure interactively.
 
-  Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
-  (\secref{sec:tool-build}).
+  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
+  (\secref{sec:tool-process}).
 
-  Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
-  (\secref{sec:tool-process}).
+  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
+  (\secref{sec:tool-build}).
 
   \<^medskip>
   The Isabelle/ML process is run through the line editor that is specified via
diff -r 751cf9f3d433 -r 699e86051e35 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 20:50:38 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 21:11:15 2016 +0100
@@ -109,6 +109,7 @@
   def main(args: Array[String])
   {
     Command_Line.tool {
+      var dirs: List[Path] = Nil
       var eval_args: List[String] = Nil
       var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
       var modes: List[String] = Nil
@@ -118,6 +119,7 @@
 Usage: isabelle process [OPTIONS]
 
   Options are:
+    -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
@@ -126,6 +128,7 @@
 
   Run the raw Isabelle ML process in batch mode.
 """,
+        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
         "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
         "l:" -> (arg => logic = arg),
@@ -135,7 +138,7 @@
       val more_args = getopts(args)
       if (args.isEmpty || !more_args.isEmpty) getopts.usage()
 
-      ML_Process(options, logic = logic, args = eval_args ::: args.toList, modes = modes).
+      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
         result().print_stdout.rc
     }
   }