src/Pure/PIDE/headless.scala

   private sealed case class Checkpoints_State(
     status: Checkpoints_State.Status.Value,
     nodes: List[Document.Node.Name])
   {
     def next(
-      dep_graph: Document.Theory_Graph[Unit],
+      dep_graph: Document.Node.Name.Graph[Unit],
       finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Checkpoints_State) =
     {
       import Checkpoints_State.Status
 
       def descendants: List[Document.Node.Name] =

       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: Option[Exn.Result[Use_Theories_Result]] = None)
     {
-      def dep_graph: Document.Theory_Graph[Unit] = dependencies.theory_graph
+      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)
 
       def watchdog: Boolean =

       }
 
 
       /* theories */
 
-      lazy val theory_graph: Document.Theory_Graph[Unit] =
-        Document.theory_graph(
+      lazy val theory_graph: Document.Node.Name.Graph[Unit] =
+        Document.Node.Name.make_graph(
           for ((name, theory) <- theories.toList)
           yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
 
       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)