src/Pure/ML/ml_process.scala
changeset 75394 42267c650205
parent 75393 87ebf5a50283
child 75590 99b7638d9177
--- 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)
+    })
 }