equal
deleted
inserted
replaced
28 { |
28 { |
29 GUI_Thread.require {} |
29 GUI_Thread.require {} |
30 |
30 |
31 Document_View.get(view.getTextArea) match { |
31 Document_View.get(view.getTextArea) match { |
32 case Some(doc_view) => |
32 case Some(doc_view) => |
33 doc_view.rich_text_area.robust_body() { |
33 doc_view.rich_text_area.robust_body(()) { |
34 val snapshot = doc_view.model.snapshot() |
34 val snapshot = doc_view.model.snapshot() |
35 if (!snapshot.is_outdated) { |
35 if (!snapshot.is_outdated) { |
36 handlers.find(_.handle(view, text, elem, doc_view, snapshot)) |
36 handlers.find(_.handle(view, text, elem, doc_view, snapshot)) |
37 } |
37 } |
38 } |
38 } |