# HG changeset patch
# User wenzelm
# Date 1567518927 -7200
# Node ID 60cb2bfea2d2cf2e66c0d1005ff2deb8d7aaa9c8
# Parent  3047b76712798d6ee02474a33730e2194aea428e
tuned important special case;

diff -r 3047b7671279 -r 60cb2bfea2d2 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)
       }
     }
   }