src/Pure/Tools/ml_process.scala
changeset 62835 1a9ce1b13b20
parent 62712 22a17cec2efe
child 62855 82859dac5f59
     1.1 --- a/src/Pure/Tools/ml_process.scala	Sun Apr 03 22:45:40 2016 +0200
     1.2 +++ b/src/Pure/Tools/ml_process.scala	Sun Apr 03 22:54:31 2016 +0200
     1.3 @@ -102,18 +102,17 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* command line entry point */
     1.8 +  /* Isabelle tool wrapper */
     1.9  
    1.10 -  def main(args: Array[String])
    1.11 +  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
    1.12    {
    1.13 -    Command_Line.tool {
    1.14 -      var dirs: List[Path] = Nil
    1.15 -      var eval_args: List[String] = Nil
    1.16 -      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    1.17 -      var modes: List[String] = Nil
    1.18 -      var options = Options.init()
    1.19 +    var dirs: List[Path] = Nil
    1.20 +    var eval_args: List[String] = Nil
    1.21 +    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    1.22 +    var modes: List[String] = Nil
    1.23 +    var options = Options.init()
    1.24  
    1.25 -      val getopts = Getopts("""
    1.26 +    val getopts = Getopts("""
    1.27  Usage: isabelle process [OPTIONS]
    1.28  
    1.29    Options are:
    1.30 @@ -127,20 +126,19 @@
    1.31  
    1.32    Run the raw Isabelle ML process in batch mode.
    1.33  """,
    1.34 -        "T:" -> (arg =>
    1.35 -          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
    1.36 -        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.37 -        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    1.38 -        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    1.39 -        "l:" -> (arg => logic = arg),
    1.40 -        "m:" -> (arg => modes = arg :: modes),
    1.41 -        "o:" -> (arg => options = options + arg))
    1.42 +      "T:" -> (arg =>
    1.43 +        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
    1.44 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.45 +      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
    1.46 +      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
    1.47 +      "l:" -> (arg => logic = arg),
    1.48 +      "m:" -> (arg => modes = arg :: modes),
    1.49 +      "o:" -> (arg => options = options + arg))
    1.50  
    1.51 -      val more_args = getopts(args)
    1.52 -      if (args.isEmpty || !more_args.isEmpty) getopts.usage()
    1.53 +    val more_args = getopts(args)
    1.54 +    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
    1.55  
    1.56 -      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
    1.57 -        result().print_stdout.rc
    1.58 -    }
    1.59 -  }
    1.60 +    ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
    1.61 +      result().print_stdout.rc
    1.62 +  })
    1.63  }