src/Pure/PIDE/document.scala
changeset 54562 301a721af68b
parent 54549 2a3053472ec3
child 55431 e0f20a44ff9d
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Nov 22 20:54:26 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Nov 22 21:13:44 2013 +0100
     1.3 @@ -127,10 +127,11 @@
     1.4        }
     1.5      }
     1.6      case class Clear[A, B]() extends Edit[A, B]
     1.7 +    case class Blob[A, B]() extends Edit[A, B]
     1.8 +
     1.9      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    1.10      case class Deps[A, B](header: Header) extends Edit[A, B]
    1.11      case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
    1.12 -    case class Blob[A, B]() extends Edit[A, B]
    1.13      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    1.14      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    1.15