tuned signature;
authorwenzelm
Sun, 15 Sep 2019 13:12:13 +0200
changeset 70887 43bdcf778cfe
parent 70886 47ca5c7550e4
child 70888 93aa546ffbac
tuned signature;
src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Sep 14 22:13:36 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 15 13:12:13 2019 +0200
@@ -141,7 +141,7 @@
     /* theories */
 
     private sealed case class Use_Theories_State(
-      dependencies: resources.Dependencies[Unit],
+      dep_graph: Document.Node.Name.Graph[Unit],
       checkpoints_state: Checkpoints_State,
       watchdog_timeout: Time,
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit],
@@ -150,8 +150,6 @@
       already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
       result: Option[Exn.Result[Use_Theories_Result]] = None)
     {
-      def dep_graph: Document.Node.Name.Graph[Unit] = dependencies.theory_graph
-
       def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State =
         copy(last_update = Time.now(), nodes_status = new_nodes_status)
 
@@ -263,7 +261,8 @@
           Checkpoints_State.init(
             if (checkpoints.isEmpty) Nil
             else dependencies.theory_graph.topological_order.filter(checkpoints(_)))
-        Synchronized(Use_Theories_State(dependencies, checkpoints_state, watchdog_timeout, commit))
+        Synchronized(
+          Use_Theories_State(dependencies.theory_graph, checkpoints_state, watchdog_timeout, commit))
       }
 
       def check_state(beyond_limit: Boolean = false)