src/Pure/PIDE/editor.scala
changeset 52978 37fbb3fde380
parent 52977 15254e32d299
child 52980 28f59ca8ce78
--- a/src/Pure/PIDE/editor.scala	Mon Aug 12 14:27:58 2013 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 14:53:16 2013 +0200
@@ -13,7 +13,7 @@
   def flush(): Unit
   def current_context: Context
   def current_node(context: Context): Option[Document.Node.Name]
-  def current_snapshot(context: Context): Option[Document.Snapshot]
+  def current_node_snapshot(context: Context): Option[Document.Snapshot]
   def node_snapshot(name: Document.Node.Name): Document.Snapshot
   def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]