| changeset 54461 | 6c360a6ade0e |
| parent 53844 | 71f103629327 |
| child 54702 | 3daeba5130f0 |
--- a/src/Pure/PIDE/editor.scala Sun Nov 17 09:30:13 2013 +0100 +++ b/src/Pure/PIDE/editor.scala Sun Nov 17 16:02:06 2013 +0100 @@ -11,6 +11,7 @@ { def session: Session def flush(): Unit + def invoke(): Unit def current_context: Context def current_node(context: Context): Option[Document.Node.Name] def current_node_snapshot(context: Context): Option[Document.Snapshot]