src/Pure/General/position.scala
changeset 56473 5b5c750e9763
parent 56468 30128d1acfbc
child 56532 3da244bc02bd
     1.1 --- a/src/Pure/General/position.scala	Tue Apr 08 20:00:53 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Tue Apr 08 20:03:00 2014 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4          case (Id(id), Range(range)) =>
     1.5            val chunk_name =
     1.6              pos match {
     1.7 -              case File(name) => Text.Chunk.File_Name(name)
     1.8 +              case File(name) => Text.Chunk.File(name)
     1.9                case _ => Text.Chunk.Default
    1.10              }
    1.11            Some((id, chunk_name, range))