src/Tools/jEdit/src/jedit_editor.scala
changeset 53844 71f103629327
parent 52980 28f59ca8ce78
child 53845 08721d7b2262
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 24 16:06:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Sep 24 16:35:01 2013 +0200
     1.3 @@ -62,8 +62,7 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  override def current_command(view: View, snapshot: Document.Snapshot)
     1.8 -    : Option[(Command, Text.Offset)] =
     1.9 +  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    1.10    {
    1.11      Swing_Thread.require()
    1.12  
    1.13 @@ -74,7 +73,11 @@
    1.14          case Some(doc_view) =>
    1.15            val node = snapshot.version.nodes(doc_view.model.node_name)
    1.16            val caret_commands = node.command_range(text_area.getCaretPosition)
    1.17 -          if (caret_commands.hasNext) Some(caret_commands.next) else None
    1.18 +          if (caret_commands.hasNext) {
    1.19 +            val (cmd0, _) = caret_commands.next
    1.20 +            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    1.21 +          }
    1.22 +          else None
    1.23          case None => None
    1.24        }
    1.25      }