diff -r a7acd2d8c2fb -r 2a9d8dcea893 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Jul 23 18:16:04 2014 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Wed Jul 23 21:01:28 2014 +0200 @@ -487,7 +487,7 @@ nodes += (name -> node2) } - (doc_edits.toList, Document.Version.make(Some(syntax), nodes)) + (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes)) } Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)