--- 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)
+ })
}