src/Pure/PIDE/text.scala
changeset 56470 8eda56033203
parent 56469 ffc94a271633
child 56473 5b5c750e9763
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 08 16:07:02 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 08 19:17:28 2014 +0200
     1.3 @@ -106,6 +106,7 @@
     1.4    {
     1.5      sealed abstract class Name
     1.6      case object Default extends Name
     1.7 +    case class Id(id: Document_ID.Generic) extends Name
     1.8      case class File_Name(file_name: String) extends Name
     1.9  
    1.10      class File(text: CharSequence) extends Chunk