isabelle process -d;
authorwenzelm
Wed Mar 16 21:11:15 2016 +0100 (2016-03-16)
changeset 62639699e86051e35
parent 62638 751cf9f3d433
child 62640 e36cbe677c17
isabelle process -d;
proper args;
src/Doc/System/Basics.thy
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Doc/System/Basics.thy	Wed Mar 16 20:50:38 2016 +0100
     1.2 +++ b/src/Doc/System/Basics.thy	Wed Mar 16 21:11:15 2016 +0100
     1.3 @@ -305,6 +305,7 @@
     1.4  \<open>Usage: isabelle process [OPTIONS]
     1.5  
     1.6    Options are:
     1.7 +    -d DIR       include session directory
     1.8      -e ML_EXPR   evaluate ML expression on startup
     1.9      -f ML_FILE   evaluate ML file on startup
    1.10      -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
    1.11 @@ -324,7 +325,8 @@
    1.12    premature exit of the ML process with return code 1.
    1.13  
    1.14    \<^medskip>
    1.15 -  Option \<^verbatim>\<open>-l\<close> specifies the logic session name.
    1.16 +  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
    1.17 +  additional directories for session roots, see also \secref{sec:tool-build}.
    1.18  
    1.19    \<^medskip>
    1.20    The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
    1.21 @@ -375,11 +377,11 @@
    1.22    abbreviates \<^verbatim>\<open>-l RAW_ML_SYSTEM\<close>, which is relevant to bootstrap
    1.23    Isabelle/Pure interactively.
    1.24  
    1.25 -  Options \<^verbatim>\<open>-d\<close> and \<^verbatim>\<open>-s\<close> have the same meaning as for @{tool build}
    1.26 -  (\secref{sec:tool-build}).
    1.27 +  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
    1.28 +  (\secref{sec:tool-process}).
    1.29  
    1.30 -  Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
    1.31 -  (\secref{sec:tool-process}).
    1.32 +  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
    1.33 +  (\secref{sec:tool-build}).
    1.34  
    1.35    \<^medskip>
    1.36    The Isabelle/ML process is run through the line editor that is specified via
     2.1 --- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 20:50:38 2016 +0100
     2.2 +++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 21:11:15 2016 +0100
     2.3 @@ -109,6 +109,7 @@
     2.4    def main(args: Array[String])
     2.5    {
     2.6      Command_Line.tool {
     2.7 +      var dirs: List[Path] = Nil
     2.8        var eval_args: List[String] = Nil
     2.9        var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    2.10        var modes: List[String] = Nil
    2.11 @@ -118,6 +119,7 @@
    2.12  Usage: isabelle process [OPTIONS]
    2.13  
    2.14    Options are:
    2.15 +    -d DIR       include session directory
    2.16      -e ML_EXPR   evaluate ML expression on startup
    2.17      -f ML_FILE   evaluate ML file on startup
    2.18      -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    2.19 @@ -126,6 +128,7 @@
    2.20  
    2.21    Run the raw Isabelle ML process in batch mode.
    2.22  """,
    2.23 +        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    2.24          "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    2.25          "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    2.26          "l:" -> (arg => logic = arg),
    2.27 @@ -135,7 +138,7 @@
    2.28        val more_args = getopts(args)
    2.29        if (args.isEmpty || !more_args.isEmpty) getopts.usage()
    2.30  
    2.31 -      ML_Process(options, logic = logic, args = eval_args ::: args.toList, modes = modes).
    2.32 +      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
    2.33          result().print_stdout.rc
    2.34      }
    2.35    }