# HG changeset patch
# User wenzelm
# Date 1380033301 -7200
# Node ID 71f103629327b463929bb0e7ffe4eb864a8876ce
# Parent  88c6e630c15fc35c0a28ebcd557a0ba32a65909f
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
tuned signature;

diff -r 88c6e630c15f -r 71f103629327 src/Pure/PIDE/editor.scala
--- 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
diff -r 88c6e630c15f -r 71f103629327 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Sep 24 16:06:12 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Sep 24 16:35:01 2013 +0200
@@ -153,7 +153,7 @@
         reset_state()
         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
         editor.current_command(editor_context, snapshot) match {
-          case Some((command, _)) =>
+          case Some(command) =>
             current_location = Some(command)
             current_query = query
             current_status = Query_Operation.Status.WAITING
diff -r 88c6e630c15f -r 71f103629327 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 24 16:06:12 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 24 16:35:01 2013 +0200
@@ -62,8 +62,7 @@
     }
   }
 
-  override def current_command(view: View, snapshot: Document.Snapshot)
-    : Option[(Command, Text.Offset)] =
+  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
   {
     Swing_Thread.require()
 
@@ -74,7 +73,11 @@
         case Some(doc_view) =>
           val node = snapshot.version.nodes(doc_view.model.node_name)
           val caret_commands = node.command_range(text_area.getCaretPosition)
-          if (caret_commands.hasNext) Some(caret_commands.next) else None
+          if (caret_commands.hasNext) {
+            val (cmd0, _) = caret_commands.next
+            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
+          }
+          else None
         case None => None
       }
     }
diff -r 88c6e630c15f -r 71f103629327 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 24 16:06:12 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 24 16:35:01 2013 +0200
@@ -55,7 +55,7 @@
         case Some(snapshot) =>
           if (follow && !snapshot.is_outdated) {
             PIDE.editor.current_command(view, snapshot) match {
-              case Some((cmd, _)) =>
+              case Some(cmd) =>
                 (snapshot, snapshot.state.command_state(snapshot.version, cmd))
               case None =>
                 (Document.Snapshot.init, Command.empty.init_state)