equal
deleted
inserted
replaced
87 } |
87 } |
88 |
88 |
89 def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = |
89 def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = |
90 for { |
90 for { |
91 (_, model) <- state.value.models.iterator |
91 (_, model) <- state.value.models.iterator |
92 Text.Info(range, entry) <- model.content.bibtex_entries.iterator |
92 info <- model.content.bibtex_entries.iterator |
93 } yield Text.Info(range, (entry, model)) |
93 } yield info.map((_, model)) |
94 |
94 |
95 override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
95 override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
96 { |
96 { |
97 val file = node_file(name) |
97 val file = node_file(name) |
98 get_model(file) match { |
98 get_model(file) match { |