equal
deleted
inserted
replaced
104 |
104 |
105 object Chunk |
105 object Chunk |
106 { |
106 { |
107 sealed abstract class Name |
107 sealed abstract class Name |
108 case object Default extends Name |
108 case object Default extends Name |
|
109 case class Id(id: Document_ID.Generic) extends Name |
109 case class File_Name(file_name: String) extends Name |
110 case class File_Name(file_name: String) extends Name |
110 |
111 |
111 class File(text: CharSequence) extends Chunk |
112 class File(text: CharSequence) extends Chunk |
112 { |
113 { |
113 val range = Range(0, text.length) |
114 val range = Range(0, text.length) |