src/Pure/PIDE/state.scala

--- a/src/Pure/PIDE/state.scala	Wed Aug 11 23:46:38 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Thu Aug 12 13:42:05 2010 +0200
@@ -100,14 +100,14 @@
                   }
                   else if (kind == Markup.ML_REF) {
                     body match {
-                      case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
+                      case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
                         state.add_markup(command.markup_node(
                           begin - 1, end - 1,
                           Command.RefInfo(
-                            Position.get_file(atts),
-                            Position.get_line(atts),
-                            Position.get_id(atts),
-                            Position.get_offset(atts))))
+                            Position.get_file(props),
+                            Position.get_line(props),
+                            Position.get_id(props),
+                            Position.get_offset(props))))
                       case _ => state
                     }
                   }