# HG changeset patch
# User wenzelm
# Date 1353780068 -3600
# Node ID 863b1dfc396c53a2af1f6bd1f5dda7eeda770e7e
# Parent  829ce6e03279521ec9fc963d1f3912dd40ba4bb2
prefer buffer_edit combinator over Java-style boilerplate;

diff -r 829ce6e03279 -r 863b1dfc396c src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 18:34:47 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Nov 24 19:01:08 2012 +0100
@@ -98,6 +98,12 @@
     finally { buffer.readUnlock() }
   }
 
+  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
+  {
+    try { buffer.beginCompoundEdit(); body }
+    finally { buffer.endCompoundEdit() }
+  }
+
 
   /* point range */
 
diff -r 829ce6e03279 -r 863b1dfc396c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 24 18:34:47 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 24 19:01:08 2012 +0100
@@ -92,17 +92,12 @@
 
           Swing_Thread.later {
             current_rendering = rendering
-
-            try {
-              getBuffer.beginCompoundEdit
+            JEdit_Lib.buffer_edit(getBuffer) {
               getBuffer.setReadOnly(false)
               setText(text)
               setCaretPosition(0)
               getBuffer.setReadOnly(true)
             }
-            finally {
-              getBuffer.endCompoundEdit
-            }
           }
         }))
     }
diff -r 829ce6e03279 -r 863b1dfc396c src/Tools/jEdit/src/sendback.scala
--- a/src/Tools/jEdit/src/sendback.scala	Sat Nov 24 18:34:47 2012 +0100
+++ b/src/Tools/jEdit/src/sendback.scala	Sat Nov 24 19:01:08 2012 +0100
@@ -34,14 +34,10 @@
                   case Some(command) =>
                     snapshot.node.command_start(command) match {
                       case Some(start) =>
-                        try {
-                          buffer.beginCompoundEdit()
+                        JEdit_Lib.buffer_edit(buffer) {
                           buffer.remove(start, command.proper_range.length)
                           buffer.insert(start, text)
                         }
-                        finally {
-                          buffer.endCompoundEdit()
-                        }
                       case None =>
                     }
                   case None =>
diff -r 829ce6e03279 -r 863b1dfc396c src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 18:34:47 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 19:01:08 2012 +0100
@@ -49,27 +49,19 @@
 
     text_area.getSelection.toList match {
       case Nil if control == "" =>
-        try {
-          buffer.beginCompoundEdit()
+        JEdit_Lib.buffer_edit(buffer) {
           val caret = text_area.getCaretPosition
           if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1)))
             text_area.backspace()
         }
-        finally {
-          buffer.endCompoundEdit()
-        }
       case Nil if control != "" =>
         text_area.setSelectedText(control)
       case sels =>
-        try {
-          buffer.beginCompoundEdit()
+        JEdit_Lib.buffer_edit(buffer) {
           sels.foreach(sel =>
             text_area.setSelectedText(sel,
               update_control_style(control, text_area.getSelectedText(sel))))
         }
-        finally {
-          buffer.endCompoundEdit()
-        }
     }
   }