# HG changeset patch
# User wenzelm
# Date 1407235358 -7200
# Node ID 287e3b1298b375f7cdbd004bf2234bd569d4cf5d
# Parent  bcc243ea48e7967824470c1d670587324f11a595
restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;

diff -r bcc243ea48e7 -r 287e3b1298b3 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Aug 05 12:14:25 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Aug 05 12:42:38 2014 +0200
@@ -232,8 +232,8 @@
     s: String)
   {
     if (!snapshot.is_outdated) {
-      snapshot.state.find_command(snapshot.version, id) match {
-        case Some((node, command)) =>
+      (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
+        case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
           node.command_start(command) match {
             case Some(start) =>
               JEdit_Lib.buffer_edit(buffer) {
@@ -248,7 +248,7 @@
               }
             case None =>
           }
-        case None =>
+        case _ =>
       }
     }
   }