src/Pure/General/position.scala
changeset 56473 5b5c750e9763
parent 56468 30128d1acfbc
child 56532 3da244bc02bd
equal deleted inserted replaced
56472:f4abde849190 56473:5b5c750e9763
    86     def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
    86     def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
    87       (pos, pos) match {
    87       (pos, pos) match {
    88         case (Id(id), Range(range)) =>
    88         case (Id(id), Range(range)) =>
    89           val chunk_name =
    89           val chunk_name =
    90             pos match {
    90             pos match {
    91               case File(name) => Text.Chunk.File_Name(name)
    91               case File(name) => Text.Chunk.File(name)
    92               case _ => Text.Chunk.Default
    92               case _ => Text.Chunk.Default
    93             }
    93             }
    94           Some((id, chunk_name, range))
    94           Some((id, chunk_name, range))
    95         case _ => None
    95         case _ => None
    96       }
    96       }