--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jun 21 14:06:16 2017 +0200
@@ -129,10 +129,7 @@
}
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- for {
- (_, model) <- state.value.models.iterator
- info <- model.content.bibtex_entries.iterator
- } yield info.map((_, model))
+ Bibtex.entries_iterator(state.value.models)
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{