tuned important special case;
authorwenzelm
Tue, 03 Sep 2019 15:55:27 +0200
changeset 70838 60cb2bfea2d2
parent 70837 3047b7671279
child 70839 9a40720750dc
tuned important special case;
src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Sep 03 15:24:04 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Tue Sep 03 15:55:27 2019 +0200
@@ -472,7 +472,8 @@
             frontier(base1, front ++ add)
           }
         }
-        frontier(theory_graph.maximals.filter(clean), Set.empty)
+        if (clean.isEmpty) Set.empty
+        else frontier(theory_graph.maximals.filter(clean), Set.empty)
       }
     }
   }