diff -r 79122bdd4404 -r 348599644887 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Jul 15 22:11:54 2016 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Jul 15 22:17:09 2016 +0200
@@ -58,7 +58,7 @@
                 if (buffer.isEditable) {
                   props match {
                     case Position.Id(id) =>
-                      Isabelle.edit_command(snapshot, buffer,
+                      Isabelle.edit_command(snapshot, text_area,
                         props.contains(Markup.PADDING_COMMAND), id, text)
                     case _ =>
                       if (props.contains(Markup.PADDING_LINE))