src/Tools/jEdit/src/jedit/document_view.scala
changeset 39636 610dc743932c
parent 39182 cce0c10ed943
child 39690 6c6164b37fef
     1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 00:00:21 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 14:12:33 2010 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    {
     1.5      Swing_Thread.require()
     1.6      apply(text_area) match {
     1.7 -      case None => error("No document view for text area: " + text_area)
     1.8 +      case None =>
     1.9        case Some(doc_view) =>
    1.10          doc_view.deactivate()
    1.11          text_area.putClientProperty(key, null)