--- 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)
--- 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)