src/Tools/jEdit/src/active.scala

                     Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                   })
 
               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)
                     else text_area.setSelectedText(text)
                 }