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)))
   }