src/Pure/General/position.scala

--- a/src/Pure/General/position.scala	Sun Aug 24 19:24:27 2008 +0200
+++ b/src/Pure/General/position.scala	Sun Aug 24 21:15:44 2008 +0200
@@ -13,7 +13,7 @@
 object Position {
 
   private def get_string(name: String, props: Properties) = {
-    val value = props.getProperty(name)
+    val value = if (props != null) props.getProperty(name) else null
     if (value != null) Some(value) else None
   }