# HG changeset patch
# User wenzelm
# Date 1282499600 -7200
# Node ID ce46a6f55bce6952fa50a8a0a3ccf3d18c498a95
# Parent  1ebc6b76e5ffded2890f51364d777625c7f07358
tuned signature;

diff -r 1ebc6b76e5ff -r ce46a6f55bce 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 */