--- 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
--- 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
}
}