| changeset 56918 | a442dc6d244d |
| parent 56715 | 52125652e82a |
| child 56919 | 6389a8c1268a |
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu May 08 21:03:05 2014 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu May 08 21:14:25 2014 +0200 @@ -24,6 +24,8 @@ val pretty_text_area = new Pretty_Text_Area(view) set_content(pretty_text_area) + override def detach_operation = pretty_text_area.detach_operation + /* query operation */