src/Pure/Tools/server_commands.scala

 */
 
 package isabelle
 
 
-object Server_Commands
-{
+object Server_Commands {
   def default_preferences: String = Options.read_prefs()
 
-  object Help extends Server.Command("help")
-  {
+  object Help extends Server.Command("help") {
     override val command_body: Server.Command_Body =
       { case (context, ()) => context.command_list }
   }
 
-  object Echo extends Server.Command("echo")
-  {
+  object Echo extends Server.Command("echo") {
     override val command_body: Server.Command_Body =
       { case (_, t) => t }
   }
 
-  object Cancel extends Server.Command("cancel")
-  {
+  object Cancel extends Server.Command("cancel") {
     sealed case class Args(task: UUID.T)
 
     def unapply(json: JSON.T): Option[Args] =
       for { task <- JSON.uuid(json, "task") }
       yield Args(task)
 
     override val command_body: Server.Command_Body =
       { case (context, Cancel(args)) => context.cancel_task(args.task) }
   }
 
-  object Shutdown extends Server.Command("shutdown")
-  {
+  object Shutdown extends Server.Command("shutdown") {
     override val command_body: Server.Command_Body =
       { case (context, ()) => context.server.shutdown() }
   }
 
-  object Session_Build extends Server.Command("session_build")
-  {
+  object Session_Build extends Server.Command("session_build") {
     sealed case class Args(
       session: String,
       preferences: String = default_preferences,
       options: List[String] = Nil,
       dirs: List[String] = Nil,

       yield {
         Args(session, preferences = preferences, options = options, dirs = dirs,
           include_sessions = include_sessions, verbose = verbose)
       }
 
-    def command(args: Args, progress: Progress = new Progress)
-      : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
-    {
+    def command(
+      args: Args,
+      progress: Progress = new Progress
+    ) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = {
       val options = Options.init(prefs = args.preferences, opts = args.options)
       val dirs = args.dirs.map(Path.explode)
 
       val base_info =
         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,

       val results_json =
         JSON.Object(
           "ok" -> results.ok,
           "return_code" -> results.rc,
           "sessions" ->
-            results.sessions.toList.sortBy(sessions_order).map(session =>
-              {
-                val result = results(session)
-                JSON.Object(
-                  "session" -> session,
-                  "ok" -> result.ok,
-                  "return_code" -> result.rc,
-                  "timeout" -> result.timeout,
-                  "timing" -> result.timing.json)
-              }))
+            results.sessions.toList.sortBy(sessions_order).map(session => {
+              val result = results(session)
+              JSON.Object(
+                "session" -> session,
+                "ok" -> result.ok,
+                "return_code" -> result.rc,
+                "timeout" -> result.timeout,
+                "timing" -> result.timing.json)
+            }))
 
       if (results.ok) (results_json, results, options, base_info)
       else {
         throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc),
           results_json)

     override val command_body: Server.Command_Body =
       { case (context, Session_Build(args)) =>
         context.make_task(task => Session_Build.command(args, progress = task.progress)._1) }
   }
 
-  object Session_Start extends Server.Command("session_start")
-  {
+  object Session_Start extends Server.Command("session_start") {
     sealed case class Args(
       build: Session_Build.Args,
       print_mode: List[String] = Nil)
 
     def unapply(json: JSON.T): Option[Args] =

         build <- Session_Build.unapply(json)
         print_mode <- JSON.strings_default(json, "print_mode")
       }
       yield Args(build = build, print_mode = print_mode)
 
-    def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger)
-      : (JSON.Object.T, (UUID.T, Headless.Session)) =
-    {
+    def command(
+      args: Args,
+      progress: Progress = new Progress,
+      log: Logger = No_Logger
+    ) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
       val (_, _, options, base_info) =
         try { Session_Build.command(args.build, progress = progress) }
         catch { case exn: Server.Error => error(exn.message) }
 
       val resources = Headless.Resources(options, base_info, log = log)

       (res, id -> session)
     }
 
     override val command_body: Server.Command_Body =
       { case (context, Session_Start(args)) =>
-          context.make_task(task =>
-          {
+          context.make_task(task => {
             val (res, entry) =
               Session_Start.command(args, progress = task.progress, log = context.server.log)
             context.server.add_session(entry)
             res
           })
       }
   }
 
-  object Session_Stop extends Server.Command("session_stop")
-  {
+  object Session_Stop extends Server.Command("session_stop") {
     def unapply(json: JSON.T): Option[UUID.T] =
       JSON.uuid(json, "session_id")
 
-    def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
-    {
+    def command(session: Headless.Session): (JSON.Object.T, Process_Result) = {
       val result = session.stop()
       val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
 
       if (result.ok) (result_json, result)
       else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json)

           Session_Stop.command(session)._1
         })
       }
   }
 
-  object Use_Theories extends Server.Command("use_theories")
-  {
+  object Use_Theories extends Server.Command("use_theories") {
     sealed case class Args(
       session_id: UUID.T,
       theories: List[String],
       master_dir: String = "",
       pretty_margin: Double = Pretty.default_margin,

       }
 
     def command(args: Args,
       session: Headless.Session,
       id: UUID.T = UUID.random(),
-      progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
-    {
+      progress: Progress = new Progress
+    ): (JSON.Object.T, Headless.Use_Theories_Result) = {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
           check_delay = args.check_delay.getOrElse(session.default_check_delay),
           check_limit = args.check_limit.getOrElse(session.default_check_limit),
           watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout),

           id = id, progress = progress)
 
       def output_text(text: String): String =
         Symbol.output(args.unicode_symbols, text)
 
-      def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
-      {
+      def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = {
         val position = "pos" -> Position.JSON(pos)
         tree match {
           case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
           case elem: XML.Elem =>
             val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))

       (result_json, result)
     }
 
     override val command_body: Server.Command_Body =
       { case (context, Use_Theories(args)) =>
-        context.make_task(task =>
-        {
+        context.make_task(task => {
           val session = context.server.the_session(args.session_id)
           Use_Theories.command(args, session, id = task.id, progress = task.progress)._1
         })
       }
   }
 
-  object Purge_Theories extends Server.Command("purge_theories")
-  {
+  object Purge_Theories extends Server.Command("purge_theories") {
     sealed case class Args(
       session_id: UUID.T,
       theories: List[String] = Nil,
       master_dir: String = "",
       all: Boolean = false)

         master_dir <- JSON.string_default(json, "master_dir")
         all <- JSON.bool_default(json, "all")
       }
       yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
 
-    def command(args: Args, session: Headless.Session)
-      : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
-    {
+    def command(
+      args: Args,
+      session: Headless.Session
+    ) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = {
       val (purged, retained) =
         session.purge_theories(
           theories = args.theories, master_dir = args.master_dir, all = args.all)
 
       val result_json =