tuned -- fewer aliases of critical operations;

--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 28 15:22:57 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 28 15:29:09 2014 +0200
@@ -94,9 +94,6 @@
 
   /* buffers */
 
-  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
-    Swing_Thread.now { buffer_lock(buffer) { body } }
-
   def buffer_text(buffer: JEditBuffer): String =
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 

--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 15:22:57 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 15:29:09 2014 +0200
@@ -126,22 +126,22 @@
     }
   }
 
-  def init_view(buffer: Buffer, text_area: JEditTextArea)
-  {
-    JEdit_Lib.swing_buffer_lock(buffer) {
-      document_model(buffer) match {
-        case Some(model) => Document_View.init(model, text_area)
-        case None =>
+  def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
+    Swing_Thread.now {
+      JEdit_Lib.buffer_lock(buffer) {
+        document_model(buffer) match {
+          case Some(model) => Document_View.init(model, text_area)
+          case None =>
+        }
       }
     }
-  }
 
-  def exit_view(buffer: Buffer, text_area: JEditTextArea)
-  {
-    JEdit_Lib.swing_buffer_lock(buffer) {
-      Document_View.exit(text_area)
+  def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
+    Swing_Thread.now {
+      JEdit_Lib.buffer_lock(buffer) {
+        Document_View.exit(text_area)
+      }
     }
-  }
 
 
   /* current document content */