changeset 34788 | 3779c54a2d21 |
parent 34784 | 02959dcea756 |
child 34789 | 30528e68f774 |
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Dec 15 20:15:54 2009 +0100 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Dec 15 20:20:07 2009 +0100 @@ -42,7 +42,7 @@ loop { react { case cmd: Command => - Document_Model.get(view.getBuffer) match { + Document_Model(view.getBuffer) match { case None => case Some(model) => val body =