# HG changeset patch
# User wenzelm
# Date 1520966082 -3600
# Node ID dd83610333de1c57a629e9378f6816c62d045330
# Parent  c61acb4855b68ae766ae27145f07b32f963fe425
added server command "session_build": similar to JEdit_Resources.session_build;

diff -r c61acb4855b6 -r dd83610333de src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Mar 13 18:40:25 2018 +0100
+++ b/src/Pure/Tools/server.scala	Tue Mar 13 19:34:42 2018 +0100
@@ -64,9 +64,13 @@
 
     private val table: Map[String, T] =
       Map(
+        "help" -> { case (_, ()) => table.keySet.toList.sorted },
         "echo" -> { case (_, t) => t },
-        "help" -> { case (_, ()) => table.keySet.toList.sorted },
-        "shutdown" -> { case (context, ()) => context.shutdown(); () })
+        "shutdown" -> { case (context, ()) => context.shutdown(); () },
+        "session_build" ->
+          { case (context, Server_Commands.Session_Build(args)) =>
+             Server_Commands.Session_Build.command(context.progress(), args)._1
+          })
 
     def unapply(name: String): Option[T] = table.get(name)
   }
diff -r c61acb4855b6 -r dd83610333de src/Pure/Tools/server_commands.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/server_commands.scala	Tue Mar 13 19:34:42 2018 +0100
@@ -0,0 +1,70 @@
+/*  Title:      Pure/Tools/server_commands.scala
+    Author:     Makarius
+
+Miscellaneous Isabelle server commands.
+*/
+
+package isabelle
+
+
+object Server_Commands
+{
+  object Session_Build
+  {
+    sealed case class Args(
+      session: String,
+      prefs: String = "",
+      opts: List[String] = Nil,
+      dirs: List[String] = Nil,
+      ancestor_session: String = "",
+      all_known: Boolean = false,
+      focus_session: Boolean = false,
+      required_session: Boolean = false,
+      system_mode: Boolean = false)
+
+    def unapply(json: JSON.T): Option[Args] =
+      for {
+        session <- JSON.string(json, "session")
+        prefs <- JSON.string_default(json, "preferences")
+        opts <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
+        dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
+        ancestor_session <- JSON.string_default(json, "ancestor_session")
+        all_known <- JSON.bool_default(json, "all_known")
+        focus_session <- JSON.bool_default(json, "focus_session")
+        required_session <- JSON.bool_default(json, "required_session")
+        system_mode <- JSON.bool_default(json, "system_mode")
+      }
+      yield {
+        Args(session, prefs = prefs, opts = opts, dirs = dirs, ancestor_session = ancestor_session,
+          all_known = all_known, focus_session = focus_session, required_session = required_session,
+          system_mode = system_mode)
+      }
+
+    def command(progress: Progress, args: Args): (JSON.T, Sessions.Base_Info, Build.Results) =
+    {
+      val options = Options.init(prefs = args.prefs, opts = args.opts)
+      val dirs = args.dirs.map(Path.explode(_))
+
+      val base_info =
+        Sessions.base_info(options,
+          args.session,
+          dirs = dirs,
+          ancestor_session = proper_string(args.ancestor_session),
+          all_known = args.all_known,
+          focus_session = args.focus_session,
+          required_session = args.required_session)
+      val base = base_info.check_base
+
+      val results =
+        Build.build(options,
+          progress = progress,
+          build_heap = true,
+          system_mode = args.system_mode,
+          dirs = dirs,
+          infos = base_info.infos,
+          sessions = List(args.session))
+
+      (Map("rc" -> results.rc), base_info, results)
+    }
+  }
+}
diff -r c61acb4855b6 -r dd83610333de src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Mar 13 18:40:25 2018 +0100
+++ b/src/Pure/build-jars	Tue Mar 13 19:34:42 2018 +0100
@@ -147,6 +147,7 @@
   Tools/print_operation.scala
   Tools/profiling_report.scala
   Tools/server.scala
+  Tools/server_commands.scala
   Tools/simplifier_trace.scala
   Tools/spell_checker.scala
   Tools/task_statistics.scala