src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Sun Aug 22 19:33:01 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Aug 22 19:53:20 2010 +0200
@@ -45,7 +45,7 @@
             msg match {
               case XML.Elem(Markup(name, atts), args)
               if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
-                val range = command.decode_range(Position.get_range(atts).get)
+                val range = command.decode(Position.get_range(atts).get)
                 val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
                 val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
                 add_markup(info)
@@ -89,7 +89,8 @@
   val range: Text.Range = Text.Range(0, length)
 
   lazy val symbol_index = new Symbol.Index(source)
-  def decode_range(r: Text.Range): Text.Range = symbol_index.decode(r)
+  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
+  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
 
 
   /* accumulated results */