src/Pure/General/symbol.scala
changeset 65335 7634d33c1a79
parent 65196 e8760a98db78
child 65344 b99283eed13c
equal deleted inserted replaced
65334:264a3904ab5a 65335:7634d33c1a79
   196     sealed abstract class Name
   196     sealed abstract class Name
   197     case object Default extends Name
   197     case object Default extends Name
   198     case class Id(id: Document_ID.Generic) extends Name
   198     case class Id(id: Document_ID.Generic) extends Name
   199     case class File(name: String) extends Name
   199     case class File(name: String) extends Name
   200 
   200 
       
   201     val encode_name: XML.Encode.T[Name] =
       
   202     {
       
   203       import XML.Encode._
       
   204       variant(List(
       
   205         { case Default => (Nil, Nil) },
       
   206         { case Id(a) => (List(long_atom(a)), Nil) },
       
   207         { case File(a) => (List(a), Nil) }))
       
   208     }
       
   209 
       
   210     val decode_name: XML.Decode.T[Name] =
       
   211     {
       
   212       import XML.Decode._
       
   213       variant(List(
       
   214         { case (Nil, Nil) => Default },
       
   215         { case (List(a), Nil) => Id(long_atom(a)) },
       
   216         { case (List(a), Nil) => File(a) }))
       
   217     }
       
   218 
       
   219 
   201     def apply(text: CharSequence): Text_Chunk =
   220     def apply(text: CharSequence): Text_Chunk =
   202       new Text_Chunk(Text.Range(0, text.length), Index(text))
   221       new Text_Chunk(Text.Range(0, text.length), Index(text))
   203   }
   222   }
   204 
   223 
   205   final class Text_Chunk private(val range: Text.Range, private val index: Index)
   224   final class Text_Chunk private(val range: Text.Range, private val index: Index)