src/Tools/jEdit/src/jedit_editor.scala
changeset 52973 d5f7fa1498b7
parent 52971 31926d2c04ee
child 52974 908e8a36e975
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:49:58 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:56:12 2013 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4      Swing_Thread.require { jEdit.getActiveView() }
     1.5  
     1.6    def current_node(view: View): Option[Document.Node.Name] =
     1.7 -    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.name) }
     1.8 +    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
     1.9  
    1.10    def current_snapshot(view: View): Option[Document.Snapshot] =
    1.11      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    1.12 @@ -35,7 +35,7 @@
    1.13        val text_area = view.getTextArea
    1.14        PIDE.document_view(text_area) match {
    1.15          case Some(doc_view) =>
    1.16 -          val node = snapshot.version.nodes(doc_view.model.name)
    1.17 +          val node = snapshot.version.nodes(doc_view.model.node_name)
    1.18            node.command_at(text_area.getCaretPosition)
    1.19          case None => None
    1.20        }