--- 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 */
--- 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
- }
}
}))
}
--- 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 =>
--- 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()
- }
}
}