src/Pure/General/position.scala
changeset 38872 26c505765024
parent 38722 ba31936497c2
child 38887 1261481ef5e5
     1.1 --- a/src/Pure/General/position.scala	Mon Aug 30 11:35:17 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Mon Aug 30 13:01:32 2010 +0200
     1.3 @@ -28,4 +28,6 @@
     1.4          case _ => None
     1.5        }
     1.6    }
     1.7 +
     1.8 +  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
     1.9  }