# HG changeset patch
# User wenzelm
# Date 1281613325 -7200
# Node ID 15819cbd7b0e1a71378579e01eefb5fc6d90870e
# Parent  715f39fd752d85bd3d8e8a5eb7d7ef77a74d27b8
tuned scope;

diff -r 715f39fd752d -r 15819cbd7b0e 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
                     }
                   }