--- a/src/Tools/jEdit/src/document_model.scala Thu Jan 12 12:29:12 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Jan 12 12:32:32 2017 +0100
@@ -428,7 +428,8 @@
/* blob */
- private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by GUI thread
+ // owned by GUI thread
+ private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None
private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
@@ -453,7 +454,8 @@
/* bibtex entries */
- private var _bibtex_entries: Option[List[Text.Info[String]]] = None // owned by GUI thread
+ // owned by GUI thread
+ private var _bibtex_entries: Option[List[Text.Info[String]]] = None
private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }