--- 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 =
{
--- 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
}
--- 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,