tuned -- fewer aliases of critical operations;
authorwenzelm
Mon Apr 28 15:29:09 2014 +0200 (2014-04-28)
changeset 567742d39c313f39e
parent 56773 5c7ade7a1e74
child 56775 59f70b89e5fd
tuned -- fewer aliases of critical operations;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 28 15:22:57 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 28 15:29:09 2014 +0200
     1.3 @@ -94,9 +94,6 @@
     1.4  
     1.5    /* buffers */
     1.6  
     1.7 -  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
     1.8 -    Swing_Thread.now { buffer_lock(buffer) { body } }
     1.9 -
    1.10    def buffer_text(buffer: JEditBuffer): String =
    1.11      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.12  
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 15:22:57 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 28 15:29:09 2014 +0200
     2.3 @@ -126,22 +126,22 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  def init_view(buffer: Buffer, text_area: JEditTextArea)
     2.8 -  {
     2.9 -    JEdit_Lib.swing_buffer_lock(buffer) {
    2.10 -      document_model(buffer) match {
    2.11 -        case Some(model) => Document_View.init(model, text_area)
    2.12 -        case None =>
    2.13 +  def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
    2.14 +    Swing_Thread.now {
    2.15 +      JEdit_Lib.buffer_lock(buffer) {
    2.16 +        document_model(buffer) match {
    2.17 +          case Some(model) => Document_View.init(model, text_area)
    2.18 +          case None =>
    2.19 +        }
    2.20        }
    2.21      }
    2.22 -  }
    2.23  
    2.24 -  def exit_view(buffer: Buffer, text_area: JEditTextArea)
    2.25 -  {
    2.26 -    JEdit_Lib.swing_buffer_lock(buffer) {
    2.27 -      Document_View.exit(text_area)
    2.28 +  def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
    2.29 +    Swing_Thread.now {
    2.30 +      JEdit_Lib.buffer_lock(buffer) {
    2.31 +        Document_View.exit(text_area)
    2.32 +      }
    2.33      }
    2.34 -  }
    2.35  
    2.36  
    2.37    /* current document content */