src/Pure/PIDE/headless.scala
changeset 70648 60cb2bfea2d2
parent 70647 3047b7671279
child 70649 9a40720750dc
equal deleted inserted replaced
70647:3047b7671279 70648:60cb2bfea2d2
   470             val pre_add = add.map(theory_graph.imm_preds)
   470             val pre_add = add.map(theory_graph.imm_preds)
   471             val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
   471             val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
   472             frontier(base1, front ++ add)
   472             frontier(base1, front ++ add)
   473           }
   473           }
   474         }
   474         }
   475         frontier(theory_graph.maximals.filter(clean), Set.empty)
   475         if (clean.isEmpty) Set.empty
       
   476         else frontier(theory_graph.maximals.filter(clean), Set.empty)
   476       }
   477       }
   477     }
   478     }
   478   }
   479   }
   479 
   480 
   480   class Resources private[Headless](
   481   class Resources private[Headless](