# HG changeset patch
# User wenzelm
# Date 1285330353 -7200
# Node ID 610dc743932c186f10ae36868f94e3fd53789073
# Parent  5cd8545a070bc760de664e8e32bcf072835967d6
permissive exit;

diff -r 5cd8545a070b -r 610dc743932c src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Sep 24 00:00:21 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Sep 24 14:12:33 2010 +0200
@@ -98,7 +98,7 @@
   {
     Swing_Thread.require()
     apply(buffer) match {
-      case None => error("No document model for buffer: " + buffer)
+      case None =>
       case Some(model) =>
         model.deactivate()
         buffer.unsetProperty(key)
diff -r 5cd8545a070b -r 610dc743932c src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 00:00:21 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 14:12:33 2010 +0200
@@ -52,7 +52,7 @@
   {
     Swing_Thread.require()
     apply(text_area) match {
-      case None => error("No document view for text area: " + text_area)
+      case None =>
       case Some(doc_view) =>
         doc_view.deactivate()
         text_area.putClientProperty(key, null)