# HG changeset patch
# User wenzelm
# Date 1537262070 -7200
# Node ID bb4e4c253ebe78fc862e3841f038ace5ecb3ff94
# Parent  c91d14ab065f03fc6e2f2da56f39806adea625e7
tuned signature;

diff -r c91d14ab065f -r bb4e4c253ebe src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Sep 18 11:05:14 2018 +0200
+++ b/src/Pure/PIDE/headless.scala	Tue Sep 18 11:14:30 2018 +0200
@@ -65,7 +65,7 @@
     snapshot
   }
 
-  class Theories_Result private[Headless](
+  class Use_Theories_Result private[Headless](
     val state: Document.State,
     val version: Document.Version,
     val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
@@ -115,7 +115,7 @@
       last_update: Time = Time.now(),
       nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
       already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
-      result: Promise[Theories_Result] = Future.promise[Theories_Result])
+      result: Promise[Use_Theories_Result] = Future.promise[Use_Theories_Result])
     {
       def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
         copy(last_update = Time.now(), nodes_status = new_nodes_status)
@@ -126,7 +126,7 @@
       def cancel_result { result.cancel }
       def finished_result: Boolean = result.is_finished
       def await_result { result.join_result }
-      def join_result: Theories_Result = result.join
+      def join_result: Use_Theories_Result = result.join
       def check_result(
           state: Document.State,
           version: Document.Version,
@@ -173,7 +173,7 @@
               status <- already_committed.get(name)
             } yield (name -> status)
 
-          try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) }
+          try { result.fulfill(new Use_Theories_Result(state, version, nodes, nodes_committed)) }
           catch { case _: IllegalStateException => }
         }
 
@@ -193,7 +193,7 @@
       // commit: must not block, must not fail
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
       commit_cleanup_delay: Time = default_commit_cleanup_delay,
-      progress: Progress = No_Progress): Theories_Result =
+      progress: Progress = No_Progress): Use_Theories_Result =
     {
       val dep_theories =
       {
diff -r c91d14ab065f -r bb4e4c253ebe src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Sep 18 11:05:14 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Sep 18 11:14:30 2018 +0200
@@ -158,7 +158,7 @@
       Headless.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
         include_sessions = include_sessions, progress = progress, log = log)
 
-    val theories_result =
+    val use_theories_result =
       session.use_theories(use_theories,
         progress = progress,
         commit = Some(Consumer.apply _),
@@ -169,7 +169,7 @@
 
     val consumer_ok = Consumer.shutdown()
 
-    if (theories_result.ok && consumer_ok) session_result
+    if (use_theories_result.ok && consumer_ok) session_result
     else session_result.error_rc
   }
 
diff -r c91d14ab065f -r bb4e4c253ebe src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue Sep 18 11:05:14 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Tue Sep 18 11:14:30 2018 +0200
@@ -188,7 +188,7 @@
     def command(args: Args,
       session: Headless.Session,
       id: UUID = UUID(),
-      progress: Progress = No_Progress): (JSON.Object.T, Headless.Theories_Result) =
+      progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
     {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,