changeset 43715 | 518e44a0ee15 |
parent 43697 | 77ce24aa1770 |
child 43722 | 9b5dadb0c28d |
--- a/src/Pure/Thy/thy_syntax.scala Sat Jul 09 12:56:51 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sat Jul 09 13:29:33 2011 +0200 @@ -194,7 +194,7 @@ inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) doc_edits += (name -> Some(cmd_edits)) - nodes += (name -> new Document.Node(node.header, commands2)) + nodes += (name -> Document.Node(node.header, node.blobs, commands2)) } (doc_edits.toList, new Document.Version(Document.new_id(), nodes)) }