prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
authorwenzelm
Sun Apr 03 22:54:31 2016 +0200 (2016-04-03)
changeset 628351a9ce1b13b20
parent 62834 970cedec9748
child 62836 98dbed6cfa44
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
lib/Tools/process
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/lib/Tools/process	Sun Apr 03 22:45:40 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,22 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# DESCRIPTION: raw ML process (batch mode)
     1.9 -
    1.10 -isabelle_admin_build jars || exit $?
    1.11 -
    1.12 -case "$ISABELLE_JAVA_PLATFORM" in
    1.13 -  x86-*)
    1.14 -    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
    1.15 -    ;;
    1.16 -  x86_64-*)
    1.17 -    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
    1.18 -    ;;
    1.19 -esac
    1.20 -
    1.21 -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    1.22 -
    1.23 -mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
    1.24 -
    1.25 -exec isabelle java isabelle.ML_Process "$@"
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:45:40 2016 +0200
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:54:31 2016 +0200
     2.3 @@ -71,6 +71,7 @@
     2.4    register(Build.isabelle_tool)
     2.5    register(Check_Sources.isabelle_tool)
     2.6    register(Doc.isabelle_tool)
     2.7 +  register(ML_Process.isabelle_tool)
     2.8    register(Options.isabelle_tool)
     2.9  
    2.10  
     3.1 --- a/src/Pure/Tools/ml_process.scala	Sun Apr 03 22:45:40 2016 +0200
     3.2 +++ b/src/Pure/Tools/ml_process.scala	Sun Apr 03 22:54:31 2016 +0200
     3.3 @@ -102,18 +102,17 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* command line entry point */
     3.8 +  /* Isabelle tool wrapper */
     3.9  
    3.10 -  def main(args: Array[String])
    3.11 +  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
    3.12    {
    3.13 -    Command_Line.tool {
    3.14 -      var dirs: List[Path] = Nil
    3.15 -      var eval_args: List[String] = Nil
    3.16 -      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    3.17 -      var modes: List[String] = Nil
    3.18 -      var options = Options.init()
    3.19 +    var dirs: List[Path] = Nil
    3.20 +    var eval_args: List[String] = Nil
    3.21 +    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    3.22 +    var modes: List[String] = Nil
    3.23 +    var options = Options.init()
    3.24  
    3.25 -      val getopts = Getopts("""
    3.26 +    val getopts = Getopts("""
    3.27  Usage: isabelle process [OPTIONS]
    3.28  
    3.29    Options are:
    3.30 @@ -127,20 +126,19 @@
    3.31  
    3.32    Run the raw Isabelle ML process in batch mode.
    3.33  """,
    3.34 -        "T:" -> (arg =>
    3.35 -          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
    3.36 -        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    3.37 -        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    3.38 -        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    3.39 -        "l:" -> (arg => logic = arg),
    3.40 -        "m:" -> (arg => modes = arg :: modes),
    3.41 -        "o:" -> (arg => options = options + arg))
    3.42 +      "T:" -> (arg =>
    3.43 +        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
    3.44 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    3.45 +      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    3.46 +      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    3.47 +      "l:" -> (arg => logic = arg),
    3.48 +      "m:" -> (arg => modes = arg :: modes),
    3.49 +      "o:" -> (arg => options = options + arg))
    3.50  
    3.51 -      val more_args = getopts(args)
    3.52 -      if (args.isEmpty || !more_args.isEmpty) getopts.usage()
    3.53 +    val more_args = getopts(args)
    3.54 +    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
    3.55  
    3.56 -      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
    3.57 -        result().print_stdout.rc
    3.58 -    }
    3.59 -  }
    3.60 +    ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
    3.61 +      result().print_stdout.rc
    3.62 +  })
    3.63  }