# HG changeset patch
# User wenzelm
# Date 1330884969 -3600
# Node ID d68ea01d5084aee9214c5167cfc35c5daae3c208
# Parent  bb7280848c992f1970e2f307db1f2f7b84675ded
removed obsolete proper_command_at (cf. 03a2dc9e0624);

diff -r bb7280848c99 -r d68ea01d5084 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Mar 04 19:03:28 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Mar 04 19:16:09 2012 +0100
@@ -158,13 +158,6 @@
       if (range.hasNext) Some(range.next) else None
     }
 
-    def proper_command_at(i: Text.Offset): Option[Command] =
-      command_at(i) match {
-        case Some((command, _)) =>
-          commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
-        case None => None
-      }
-
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.command_starts(commands.iterator).find(_._1 == cmd).map(_._2)
   }
diff -r bb7280848c99 -r d68ea01d5084 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sun Mar 04 19:03:28 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Mar 04 19:16:09 2012 +0100
@@ -336,7 +336,7 @@
   def selected_command(): Option[Command] =
   {
     Swing_Thread.require()
-    update_snapshot().node.proper_command_at(text_area.getCaretPosition)
+    update_snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
   }
 
   private val delay_caret_update =