# HG changeset patch
# User wenzelm
# Date 1458335986 -3600
# Node ID 0df43889f49617ceabca59af213435bde903e4f7
# Parent  1792f8ed2b04c655f92735fecf980d9205a6deec
isabelle process -T THEORY;

diff -r 1792f8ed2b04 -r 0df43889f496 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Fri Mar 18 22:15:51 2016 +0100
+++ b/src/Doc/System/Environment.thy	Fri Mar 18 22:19:46 2016 +0100
@@ -305,6 +305,7 @@
 \<open>Usage: isabelle process [OPTIONS]
 
   Options are:
+    -T THEORY    load theory
     -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
@@ -321,6 +322,10 @@
   premature exit of the ML process with return code 1.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with
+  a suitable @{ML use_thy} invocation.
+
+  \<^medskip>
   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}.
 
diff -r 1792f8ed2b04 -r 0df43889f496 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Mar 18 22:15:51 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Mar 18 22:19:46 2016 +0100
@@ -159,7 +159,7 @@
 
 my $cmd =
   "isabelle process -o quick_and_dirty -o threads=1" .
-  " -e 'use_thy \"$path/$new_thy_name\"' -l $mirabelle_logic" . $quiet;
+  " -T \"$path/$new_thy_name\" -l $mirabelle_logic" . $quiet;
 my $result = system "bash", "-c", $cmd;
 
 if ($output_log) {
diff -r 1792f8ed2b04 -r 0df43889f496 src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Mar 18 22:15:51 2016 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Mar 18 22:19:46 2016 +0100
@@ -134,7 +134,7 @@
 # execution
 
 isabelle process -o auto_time_limit=10.0 \
-  -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
+  -T "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test" -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
 
 
 [ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
diff -r 1792f8ed2b04 -r 0df43889f496 src/HOL/TPTP/CASC/ReadMe
--- a/src/HOL/TPTP/CASC/ReadMe	Fri Mar 18 22:15:51 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe	Fri Mar 18 22:19:46 2016 +0100
@@ -180,7 +180,7 @@
 
   Then I ran
 
-    ./bin/isabelle process -e 'use_thy "/tmp/T";'  
+    ./bin/isabelle process -T /tmp/T
 
   I also performed the aforementioned sanity tests.
 
diff -r 1792f8ed2b04 -r 0df43889f496 src/HOL/TPTP/lib/Tools/tptp_graph
--- a/src/HOL/TPTP/lib/Tools/tptp_graph	Fri Mar 18 22:15:51 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Fri Mar 18 22:19:46 2016 +0100
@@ -118,7 +118,7 @@
 begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
 ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
         > $WORKDIR/$LOADER.thy
-  isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" -l Pure
+  isabelle process -T "$WORKDIR/$LOADER" -l Pure
 }
 
 function cleanup_workdir()
diff -r 1792f8ed2b04 -r 0df43889f496 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Fri Mar 18 22:15:51 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Fri Mar 18 22:19:46 2016 +0100
@@ -118,6 +118,7 @@
 Usage: isabelle process [OPTIONS]
 
   Options are:
+    -T THEORY    load theory
     -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
@@ -127,6 +128,8 @@
 
   Run the raw Isabelle ML process in batch mode.
 """,
+        "T:" -> (arg =>
+          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
         "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)),