equal
deleted
inserted
replaced
426 } |
426 } |
427 |
427 |
428 |
428 |
429 /* blob */ |
429 /* blob */ |
430 |
430 |
431 private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by GUI thread |
431 // owned by GUI thread |
|
432 private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None |
432 |
433 |
433 private def reset_blob(): Unit = GUI_Thread.require { _blob = None } |
434 private def reset_blob(): Unit = GUI_Thread.require { _blob = None } |
434 |
435 |
435 def get_blob: Option[Document.Blob] = |
436 def get_blob: Option[Document.Blob] = |
436 GUI_Thread.require { |
437 GUI_Thread.require { |
451 } |
452 } |
452 |
453 |
453 |
454 |
454 /* bibtex entries */ |
455 /* bibtex entries */ |
455 |
456 |
456 private var _bibtex_entries: Option[List[Text.Info[String]]] = None // owned by GUI thread |
457 // owned by GUI thread |
|
458 private var _bibtex_entries: Option[List[Text.Info[String]]] = None |
457 |
459 |
458 private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } |
460 private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } |
459 |
461 |
460 def bibtex_entries: List[Text.Info[String]] = |
462 def bibtex_entries: List[Text.Info[String]] = |
461 GUI_Thread.require { |
463 GUI_Thread.require { |