# HG changeset patch
# User wenzelm
# Date 1406142088 -7200
# Node ID 2a9d8dcea893fc4c30008b6609adaae782d1821f
# Parent  a7acd2d8c2fb0cdd0fb0e44aa0b2401883db4531
more frugal edits;

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)