# HG changeset patch
# User wenzelm
# Date 1569835371 -7200
# Node ID b196f7d724b329f499781444343fa0542ff0022b
# Parent  5006ca9aadbba3eb68792c71c9fc7e97ee4c39f8
tuned;

diff -r 5006ca9aadbb -r b196f7d724b3 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Sep 29 16:44:29 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 30 11:22:51 2019 +0200
@@ -54,16 +54,16 @@
         this match {
           case Load_Init(Nil) =>
             (dep_graph.topological_order, Load_Finished)
-          case Load_Init(target :: rest) =>
-            (dep_graph.all_preds(List(target)).reverse, Load_Target(target, rest))
-          case Load_Target(target, rest) if finished(target) =>
+          case Load_Init(target :: checkpoints) =>
+            (dep_graph.all_preds(List(target)).reverse, Load_Target(target, checkpoints))
+          case Load_Target(target, checkpoints) if finished(target) =>
             val dep_graph1 =
-              if (rest.isEmpty) dep_graph
-              else dep_graph.exclude(dep_graph.all_succs(rest).toSet)
+              if (checkpoints.isEmpty) dep_graph
+              else dep_graph.exclude(dep_graph.all_succs(checkpoints).toSet)
             val descendants = dep_graph1.all_succs(List(target))
-            (descendants, Load_Descendants(descendants, rest))
-          case Load_Descendants(descendants, rest) if descendants.forall(finished) =>
-            Load_Init(rest).next(dep_graph, finished)
+            (descendants, Load_Descendants(descendants, checkpoints))
+          case Load_Descendants(descendants, checkpoints) if descendants.forall(finished) =>
+            Load_Init(checkpoints).next(dep_graph, finished)
           case st => (Nil, st)
         }
       (load_theories.filterNot(finished), st1)
@@ -71,9 +71,9 @@
   }
   private case class Load_Init(checkpoints: List[Document.Node.Name]) extends Load_State
   private case class Load_Target(
-    target: Document.Node.Name, rest: List[Document.Node.Name]) extends Load_State
+    target: Document.Node.Name, checkpoints: List[Document.Node.Name]) extends Load_State
   private case class Load_Descendants(
-    descendants: List[Document.Node.Name], rest: List[Document.Node.Name]) extends Load_State
+    descendants: List[Document.Node.Name], checkpoints: List[Document.Node.Name]) extends Load_State
   private case object Load_Finished extends Load_State
 
   class Session private[Headless](