more frugal edits;
authorwenzelm
Wed Jul 23 21:01:28 2014 +0200 (2014-07-23)
changeset 576252a9d8dcea893
parent 57624 a7acd2d8c2fb
child 57626 2288a6f17930
more frugal edits;
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Jul 23 18:16:04 2014 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Jul 23 21:01:28 2014 +0200
     1.3 @@ -487,7 +487,7 @@
     1.4  
     1.5              nodes += (name -> node2)
     1.6          }
     1.7 -        (doc_edits.toList, Document.Version.make(Some(syntax), nodes))
     1.8 +        (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
     1.9        }
    1.10  
    1.11      Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)