diff -r 5adc68deb322 -r bbd2fa353809 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Wed Nov 20 23:00:18 2013 +0100
+++ b/src/Tools/jEdit/src/active.scala	Thu Nov 21 21:55:29 2013 +0100
@@ -52,9 +52,9 @@
 
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                 props match {
-                  case Position.Id(exec_id) =>
+                  case Position.Id(id) =>
                     Isabelle.edit_command(snapshot, buffer,
-                      props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
+                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
                   case _ =>
                     if (props.exists(_ == Markup.PADDING_LINE))
                       Isabelle.insert_line_padding(text_area, text)