# HG changeset patch
# User wenzelm
# Date 1334858088 -7200
# Node ID 0692eea09cb7c1d4c27386ecf1ae447ba9b8ada0
# Parent  3b89d59a944b75475e24db052269c2c80c357049
more robust wrt. exceptions;

diff -r 3b89d59a944b -r 0692eea09cb7 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Apr 19 15:47:32 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Apr 19 19:54:48 2012 +0200
@@ -44,10 +44,12 @@
                   snapshot.node.command_start(cmd) match {
                     case Some(start) if !snapshot.is_outdated =>
                       val text = Pretty.string_of(sendback)
-                      buffer.beginCompoundEdit()
-                      buffer.remove(start, cmd.proper_range.length)
-                      buffer.insert(start, text)
-                      buffer.endCompoundEdit()
+                      try {
+                        buffer.beginCompoundEdit()
+                        buffer.remove(start, cmd.proper_range.length)
+                        buffer.insert(start, text)
+                      }
+                      finally { buffer.endCompoundEdit() }
                     case _ =>
                   }
                 case None =>