isabelle process -T THEORY;
authorwenzelm
Fri Mar 18 22:19:46 2016 +0100 (2016-03-18)
changeset 626770df43889f496
parent 62676 1792f8ed2b04
child 62678 843ff6f1de38
isabelle process -T THEORY;
src/Doc/System/Environment.thy
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
src/HOL/Mutabelle/lib/Tools/mutabelle
src/HOL/TPTP/CASC/ReadMe
src/HOL/TPTP/lib/Tools/tptp_graph
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Doc/System/Environment.thy	Fri Mar 18 22:15:51 2016 +0100
     1.2 +++ b/src/Doc/System/Environment.thy	Fri Mar 18 22:19:46 2016 +0100
     1.3 @@ -305,6 +305,7 @@
     1.4  \<open>Usage: isabelle process [OPTIONS]
     1.5  
     1.6    Options are:
     1.7 +    -T THEORY    load theory
     1.8      -d DIR       include session directory
     1.9      -e ML_EXPR   evaluate ML expression on startup
    1.10      -f ML_FILE   evaluate ML file on startup
    1.11 @@ -321,6 +322,10 @@
    1.12    premature exit of the ML process with return code 1.
    1.13  
    1.14    \<^medskip>
    1.15 +  Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with
    1.16 +  a suitable @{ML use_thy} invocation.
    1.17 +
    1.18 +  \<^medskip>
    1.19    Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
    1.20    additional directories for session roots, see also \secref{sec:tool-build}.
    1.21  
     2.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Mar 18 22:15:51 2016 +0100
     2.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Mar 18 22:19:46 2016 +0100
     2.3 @@ -159,7 +159,7 @@
     2.4  
     2.5  my $cmd =
     2.6    "isabelle process -o quick_and_dirty -o threads=1" .
     2.7 -  " -e 'use_thy \"$path/$new_thy_name\"' -l $mirabelle_logic" . $quiet;
     2.8 +  " -T \"$path/$new_thy_name\" -l $mirabelle_logic" . $quiet;
     2.9  my $result = system "bash", "-c", $cmd;
    2.10  
    2.11  if ($output_log) {
     3.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Mar 18 22:15:51 2016 +0100
     3.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Mar 18 22:19:46 2016 +0100
     3.3 @@ -134,7 +134,7 @@
     3.4  # execution
     3.5  
     3.6  isabelle process -o auto_time_limit=10.0 \
     3.7 -  -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
     3.8 +  -T "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test" -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
     3.9  
    3.10  
    3.11  [ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
     4.1 --- a/src/HOL/TPTP/CASC/ReadMe	Fri Mar 18 22:15:51 2016 +0100
     4.2 +++ b/src/HOL/TPTP/CASC/ReadMe	Fri Mar 18 22:19:46 2016 +0100
     4.3 @@ -180,7 +180,7 @@
     4.4  
     4.5    Then I ran
     4.6  
     4.7 -    ./bin/isabelle process -e 'use_thy "/tmp/T";'  
     4.8 +    ./bin/isabelle process -T /tmp/T
     4.9  
    4.10    I also performed the aforementioned sanity tests.
    4.11  
     5.1 --- a/src/HOL/TPTP/lib/Tools/tptp_graph	Fri Mar 18 22:15:51 2016 +0100
     5.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Fri Mar 18 22:19:46 2016 +0100
     5.3 @@ -118,7 +118,7 @@
     5.4  begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
     5.5  ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
     5.6          > $WORKDIR/$LOADER.thy
     5.7 -  isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" -l Pure
     5.8 +  isabelle process -T "$WORKDIR/$LOADER" -l Pure
     5.9  }
    5.10  
    5.11  function cleanup_workdir()
     6.1 --- a/src/Pure/Tools/ml_process.scala	Fri Mar 18 22:15:51 2016 +0100
     6.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Mar 18 22:19:46 2016 +0100
     6.3 @@ -118,6 +118,7 @@
     6.4  Usage: isabelle process [OPTIONS]
     6.5  
     6.6    Options are:
     6.7 +    -T THEORY    load theory
     6.8      -d DIR       include session directory
     6.9      -e ML_EXPR   evaluate ML expression on startup
    6.10      -f ML_FILE   evaluate ML file on startup
    6.11 @@ -127,6 +128,8 @@
    6.12  
    6.13    Run the raw Isabelle ML process in batch mode.
    6.14  """,
    6.15 +        "T:" -> (arg =>
    6.16 +          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
    6.17          "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    6.18          "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    6.19          "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),