src/Pure/PIDE/editor.scala
changeset 53844 71f103629327
parent 52980 28f59ca8ce78
child 54461 6c360a6ade0e
--- a/src/Pure/PIDE/editor.scala	Tue Sep 24 16:06:12 2013 +0200
+++ b/src/Pure/PIDE/editor.scala	Tue Sep 24 16:35:01 2013 +0200
@@ -15,7 +15,7 @@
   def current_node(context: Context): Option[Document.Node.Name]
   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)]
+  def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
 
   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit