prefer buffer_edit combinator over Java-style boilerplate;
authorwenzelm
Sat Nov 24 19:01:08 2012 +0100 (2012-11-24)
changeset 50195863b1dfc396c
parent 50194 829ce6e03279
child 50196 94886ebf090f
prefer buffer_edit combinator over Java-style boilerplate;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/sendback.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 18:34:47 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 19:01:08 2012 +0100
     1.3 @@ -98,6 +98,12 @@
     1.4      finally { buffer.readUnlock() }
     1.5    }
     1.6  
     1.7 +  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
     1.8 +  {
     1.9 +    try { buffer.beginCompoundEdit(); body }
    1.10 +    finally { buffer.endCompoundEdit() }
    1.11 +  }
    1.12 +
    1.13  
    1.14    /* point range */
    1.15  
     2.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 24 18:34:47 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 24 19:01:08 2012 +0100
     2.3 @@ -92,17 +92,12 @@
     2.4  
     2.5            Swing_Thread.later {
     2.6              current_rendering = rendering
     2.7 -
     2.8 -            try {
     2.9 -              getBuffer.beginCompoundEdit
    2.10 +            JEdit_Lib.buffer_edit(getBuffer) {
    2.11                getBuffer.setReadOnly(false)
    2.12                setText(text)
    2.13                setCaretPosition(0)
    2.14                getBuffer.setReadOnly(true)
    2.15              }
    2.16 -            finally {
    2.17 -              getBuffer.endCompoundEdit
    2.18 -            }
    2.19            }
    2.20          }))
    2.21      }
     3.1 --- a/src/Tools/jEdit/src/sendback.scala	Sat Nov 24 18:34:47 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/sendback.scala	Sat Nov 24 19:01:08 2012 +0100
     3.3 @@ -34,14 +34,10 @@
     3.4                    case Some(command) =>
     3.5                      snapshot.node.command_start(command) match {
     3.6                        case Some(start) =>
     3.7 -                        try {
     3.8 -                          buffer.beginCompoundEdit()
     3.9 +                        JEdit_Lib.buffer_edit(buffer) {
    3.10                            buffer.remove(start, command.proper_range.length)
    3.11                            buffer.insert(start, text)
    3.12                          }
    3.13 -                        finally {
    3.14 -                          buffer.endCompoundEdit()
    3.15 -                        }
    3.16                        case None =>
    3.17                      }
    3.18                    case None =>
     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 18:34:47 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 19:01:08 2012 +0100
     4.3 @@ -49,27 +49,19 @@
     4.4  
     4.5      text_area.getSelection.toList match {
     4.6        case Nil if control == "" =>
     4.7 -        try {
     4.8 -          buffer.beginCompoundEdit()
     4.9 +        JEdit_Lib.buffer_edit(buffer) {
    4.10            val caret = text_area.getCaretPosition
    4.11            if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
    4.12              text_area.backspace()
    4.13          }
    4.14 -        finally {
    4.15 -          buffer.endCompoundEdit()
    4.16 -        }
    4.17        case Nil if control != "" =>
    4.18          text_area.setSelectedText(control)
    4.19        case sels =>
    4.20 -        try {
    4.21 -          buffer.beginCompoundEdit()
    4.22 +        JEdit_Lib.buffer_edit(buffer) {
    4.23            sels.foreach(sel =>
    4.24              text_area.setSelectedText(sel,
    4.25                update_control_style(control, text_area.getSelectedText(sel))))
    4.26          }
    4.27 -        finally {
    4.28 -          buffer.endCompoundEdit()
    4.29 -        }
    4.30      }
    4.31    }
    4.32