author | wenzelm |
Wed, 23 Jul 2014 21:01:28 +0200 | |
changeset 58967 | 2a9d8dcea893 |
parent 58966 | a7acd2d8c2fb |
child 58968 | 2288a6f17930 |
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)