src/Tools/jEdit/src/document_model.scala
changeset 76791 c36d666ee5ee
parent 76790 7a0438979e85
child 76792 23f433294173
equal deleted inserted replaced
76790:7a0438979e85 76791:c36d666ee5ee
   612     def get_bibtex_entries: Bibtex.Entries = GUI_Thread.require {
   612     def get_bibtex_entries: Bibtex.Entries = GUI_Thread.require {
   613       if (File.is_bib(node_name.node)) {
   613       if (File.is_bib(node_name.node)) {
   614         bibtex_entries getOrElse {
   614         bibtex_entries getOrElse {
   615           val text = JEdit_Lib.buffer_text(buffer)
   615           val text = JEdit_Lib.buffer_text(buffer)
   616           val entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
   616           val entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
   617           if (entries.errors.nonEmpty) Output.warning(cat_lines(entries.errors))
       
   618           bibtex_entries = Some(entries)
   617           bibtex_entries = Some(entries)
   619           entries
   618           entries
   620         }
   619         }
   621       }
   620       }
   622       else Bibtex.Entries.empty
   621       else Bibtex.Entries.empty