diff -r 87ebf5a50283 -r 42267c650205 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Fri Apr 01 17:06:10 2022 +0200 +++ b/src/Pure/ML/ml_process.scala Fri Apr 01 23:19:12 2022 +0200 @@ -129,26 +129,27 @@ cwd = cwd, env = bash_env, redirect = redirect, - cleanup = () => { - isabelle_process_options.delete - init_session.delete - Isabelle_System.rm_tree(isabelle_tmp) - cleanup() - }) + cleanup = { () => + isabelle_process_options.delete + init_session.delete + Isabelle_System.rm_tree(isabelle_tmp) + cleanup() + }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", - Scala_Project.here, args => { - var dirs: List[Path] = Nil - var eval_args: List[String] = Nil - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") - var modes: List[String] = Nil - var options = Options.init() + Scala_Project.here, + { args => + var dirs: List[Path] = Nil + var eval_args: List[String] = Nil + var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var modes: List[String] = Nil + var options = Options.init() - val getopts = Getopts(""" + val getopts = Getopts(""" Usage: isabelle process [OPTIONS] Options are: @@ -162,27 +163,26 @@ Run the raw Isabelle ML process in batch mode. """, - "T:" -> (arg => - eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(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)), - "l:" -> (arg => logic = arg), - "m:" -> (arg => modes = arg :: modes), - "o:" -> (arg => options = options + arg)) + "T:" -> (arg => + eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(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)), + "l:" -> (arg => logic = arg), + "m:" -> (arg => modes = arg :: modes), + "o:" -> (arg => options = options + arg)) - val more_args = getopts(args) - if (args.isEmpty || more_args.nonEmpty) getopts.usage() + val more_args = getopts(args) + if (args.isEmpty || more_args.nonEmpty) getopts.usage() - val base_info = Sessions.base_info(options, logic, dirs = dirs).check - val store = Sessions.store(options) - val result = - ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args, - modes = modes, session_base = Some(base_info.base)) - .result( - progress_stdout = Output.writeln(_, stdout = true), - progress_stderr = Output.writeln(_)) + val base_info = Sessions.base_info(options, logic, dirs = dirs).check + val store = Sessions.store(options) + val result = + ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args, + modes = modes, session_base = Some(base_info.base)).result( + progress_stdout = Output.writeln(_, stdout = true), + progress_stderr = Output.writeln(_)) - sys.exit(result.rc) - }) + sys.exit(result.rc) + }) }