src/Pure/PIDE/protocol.scala
changeset 54509 1f77110c94ef
parent 52931 ac6648c0c0fb
child 54515 570ba266f5b5
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Nov 18 09:45:50 2013 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Nov 18 17:16:56 2013 +0100
     1.3 @@ -335,6 +335,7 @@
     1.4        def encode_edit(name: Document.Node.Name)
     1.5            : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
     1.6          variant(List(
     1.7 +          // FIXME Document.Node.Blob (!??)
     1.8            { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
     1.9            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    1.10            { case Document.Node.Deps(header) =>