src/Tools/jEdit/src/jedit_editor.scala
changeset 52978 37fbb3fde380
parent 52977 15254e32d299
child 52980 28f59ca8ce78
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:27:58 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:53:16 2013 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4    def current_node(view: View): Option[Document.Node.Name] =
     1.5      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
     1.6  
     1.7 -  def current_snapshot(view: View): Option[Document.Snapshot] =
     1.8 +  def current_node_snapshot(view: View): Option[Document.Snapshot] =
     1.9      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    1.10  
    1.11    def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    1.12 @@ -72,7 +72,8 @@
    1.13        PIDE.document_view(text_area) match {
    1.14          case Some(doc_view) =>
    1.15            val node = snapshot.version.nodes(doc_view.model.node_name)
    1.16 -          node.command_at(text_area.getCaretPosition)
    1.17 +          val caret_commands = node.command_range(text_area.getCaretPosition)
    1.18 +          if (caret_commands.hasNext) Some(caret_commands.next) else None
    1.19          case None => None
    1.20        }
    1.21      }