# HG changeset patch
# User wenzelm
# Date 1484220752 -3600
# Node ID 205274ca16ee141537ba29babf1834abace3e4eb
# Parent  b2e78c0ce5376fcaa33d84206a0f7bb73b87be8c
tuned whitespace;

diff -r b2e78c0ce537 -r 205274ca16ee src/Tools/jEdit/src/document_model.scala
--- 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 }