# HG changeset patch
# User wenzelm
# Date 1521222155 -3600
# Node ID 171e7735ce2581639944ab47c1c693f766051373
# Parent  7eb4c966e156ea8453bc1589c71b51ebfc8a3ce0
support for "use_theories";

diff -r 7eb4c966e156 -r 171e7735ce25 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Mar 16 17:16:09 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Mar 16 18:42:35 2018 +0100
@@ -146,6 +146,11 @@
   {
     def total: Int = unprocessed + running + warned + failed + finished
     def ok: Boolean = failed == 0
+
+    def json: JSON.Object.T =
+      JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
+        "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
+        "total" -> total, "ok" -> ok)
   }
 
   def node_status(
diff -r 7eb4c966e156 -r 171e7735ce25 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Mar 16 17:16:09 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 16 18:42:35 2018 +0100
@@ -51,10 +51,11 @@
   }
 
   sealed case class Theories_Result(
-    val requirements: List[Document.Node.Name],
-    val version: Document.Version,
-    val state: Document.State)
+    val nodes: List[(Document.Node.Name, Protocol.Node_Status)],
+    val state: Document.State,
+    val version: Document.Version)
   {
+    def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
   }
 
   class Session private[Thy_Resources](
@@ -80,7 +81,10 @@
         val state = session.current_state()
         state.stable_tip_version match {
           case Some(version) if requirements.forall(state.node_consolidated(version, _)) =>
-            try { result.fulfill(Theories_Result(requirements, version, state)) }
+            def status(name: Document.Node.Name): Protocol.Node_Status =
+              Protocol.node_status(state, version, name, version.nodes(name))
+            val nodes = for (name <- requirements) yield (name -> status(name))
+            try { result.fulfill(Theories_Result(nodes, state, version)) }
             catch { case _: IllegalStateException => }
           case _ =>
         }
diff -r 7eb4c966e156 -r 171e7735ce25 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 16 17:16:09 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 16 18:42:35 2018 +0100
@@ -91,6 +91,14 @@
                   val session = context.server.remove_session(id)
                   Server_Commands.Session_Stop.command(session)._1
                 })
+          },
+        "use_theories" ->
+          { case (context, Server_Commands.Use_Theories(args)) =>
+              context.make_task(task =>
+                {
+                  val session = context.server.the_session(args.session_id)
+                  Server_Commands.Use_Theories.command(args, session, progress = task.progress)._1
+                })
           })
 
     def unapply(name: String): Option[T] = table.get(name)
@@ -465,14 +473,16 @@
   server =>
 
   private val _sessions = Synchronized(Map.empty[String, Thy_Resources.Session])
+  def err_session(id: String): Nothing = error("No session " + Library.single_quote(id))
+  def the_session(id: String): Thy_Resources.Session =
+    _sessions.value.get(id) getOrElse err_session(id)
   def add_session(entry: (String, Thy_Resources.Session)) { _sessions.change(_ + entry) }
-  def get_session(id: String): Option[Thy_Resources.Session] = { _sessions.value.get(id) }
   def remove_session(id: String): Thy_Resources.Session =
   {
     _sessions.change_result(sessions =>
       sessions.get(id) match {
         case Some(session) => (session, sessions - id)
-        case None => error("No session " + Library.single_quote(id))
+        case None => err_session(id)
       })
   }
 
diff -r 7eb4c966e156 -r 171e7735ce25 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 16 17:16:09 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 16 18:42:35 2018 +0100
@@ -10,6 +10,18 @@
 object Server_Commands
 {
   def default_preferences: String = Options.read_prefs()
+  def default_qualifier: String = Sessions.DRAFT
+
+  def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
+    json match {
+      case JSON.Value.String(name) => Some((name, Position.none))
+      case JSON.Object(map) if map.keySet == Set("name", "pos") =>
+      (map("name"), map("pos")) match {
+        case (JSON.Value.String(name), Position.JSON(pos)) => Some((name, pos))
+        case _ => None
+      }
+      case _ => None
+    }
 
   object Session_Build
   {
@@ -140,4 +152,39 @@
       else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
     }
   }
+
+  object Use_Theories
+  {
+    sealed case class Args(
+      session_id: String,
+      theories: List[(String, Position.T)],
+      qualifier: String = default_qualifier,
+      master_dir: String = "")
+
+    def unapply(json: JSON.T): Option[Args] =
+      for {
+        session_id <- JSON.string(json, "session_id")
+        theories <- JSON.list(json, "theories", unapply_name_pos _)
+        qualifier <- JSON.string_default(json, "qualifier", default_qualifier)
+        master_dir <- JSON.string_default(json, "master_dir")
+      }
+      yield Args(session_id, theories, qualifier = qualifier, master_dir = master_dir)
+
+    def command(args: Args, session: Thy_Resources.Session, progress: Progress = No_Progress)
+      : (JSON.Object.T, Thy_Resources.Theories_Result) =
+    {
+      val result =
+        session.use_theories(args.theories, qualifier = args.qualifier,
+          master_dir = args.master_dir, progress = progress)
+
+      val result_json =
+        JSON.Object(
+          "ok" -> result.ok,
+          "nodes" ->
+            (for ((name, st) <- result.nodes) yield
+              JSON.Object("node_name" -> name.node, "theory" -> name.theory, "status" -> st.json)))
+
+      (result_json, result)
+    }
+  }
 }