src/Pure/PIDE/editor.scala
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]