1.1 --- a/src/Pure/PIDE/state.scala	Wed Aug 11 23:46:38 2010 +0200
     1.2 +++ b/src/Pure/PIDE/state.scala	Thu Aug 12 13:42:05 2010 +0200
     1.3 @@ -100,14 +100,14 @@
     1.4                    }
     1.5                    else if (kind == Markup.ML_REF) {
     1.6                      body match {
     1.7 -                      case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
     1.8 +                      case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
     1.9                          state.add_markup(command.markup_node(
    1.10                            begin - 1, end - 1,
    1.11                            Command.RefInfo(
    1.12 -                            Position.get_file(atts),
    1.13 -                            Position.get_line(atts),
    1.14 -                            Position.get_id(atts),
    1.15 -                            Position.get_offset(atts))))
    1.16 +                            Position.get_file(props),
    1.17 +                            Position.get_line(props),
    1.18 +                            Position.get_id(props),
    1.19 +                            Position.get_offset(props))))
    1.20                        case _ => state
    1.21                      }
    1.22                    }