changeset 64524 | e6a3c55b929b |
parent 64521 | 1aef5a0e18d7 |
child 64663 | 4c9fb4d4bca3 |
--- a/src/Pure/PIDE/editor.scala Thu Nov 24 11:33:55 2016 +0100 +++ b/src/Pure/PIDE/editor.scala Thu Nov 24 15:21:54 2016 +0100 @@ -12,7 +12,7 @@ def session: Session def flush(hidden: Boolean = true): Unit def invoke(): Unit - def invoke_update(): Unit + def invoke_generated(): Unit def current_context: Context def current_node(context: Context): Option[Document.Node.Name] def current_node_snapshot(context: Context): Option[Document.Snapshot]