| changeset 55431 | e0f20a44ff9d |
| parent 54562 | 301a721af68b |
| child 55432 | 9c53198dbb1c |
--- a/src/Pure/PIDE/document.scala Tue Feb 11 15:55:05 2014 +0100 +++ b/src/Pure/PIDE/document.scala Tue Feb 11 17:44:29 2014 +0100 @@ -47,7 +47,7 @@ type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[Command.Edit, Command.Perspective] - type Blobs = Map[Node.Name, Bytes] + type Blobs = Map[Node.Name, (Bytes, Command.File)] object Node {