diff -r c2c1e5944536 -r 393a37003851 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Aug 10 13:33:07 2012 +0200 +++ b/src/Pure/System/session.scala Fri Aug 10 15:14:45 2012 +0200 @@ -453,7 +453,7 @@ header: Document.Node.Header, perspective: Text.Perspective, text: String) { edit(List(header_edit(name, header), - name -> Document.Node.Clear(), // FIXME diff wrt. existing node + name -> Document.Node.Clear(), name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), name -> Document.Node.Perspective(perspective))) }