--- 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)