changeset 71775 | 291c46bf3000 |
parent 71742 | de37910974da |
child 73340 | 0ffcad1f6130 |
--- a/src/Tools/jEdit/src/active.scala Tue Apr 21 19:07:11 2020 +0200 +++ b/src/Tools/jEdit/src/active.scala Tue Apr 21 19:07:49 2020 +0200 @@ -30,7 +30,7 @@ Document_View.get(view.getTextArea) match { case Some(doc_view) => - doc_view.rich_text_area.robust_body() { + doc_view.rich_text_area.robust_body(()) { val snapshot = doc_view.model.snapshot() if (!snapshot.is_outdated) { handlers.find(_.handle(view, text, elem, doc_view, snapshot))