diff -r 15254e32d299 -r 37fbb3fde380 src/Pure/PIDE/editor.scala --- 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)]