src/Pure/PIDE/command.scala
changeset 38579 ce46a6f55bce
parent 38577 4e4d3ea3725a
child 38581 d503a0912e14
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 22 19:33:01 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 22 19:53:20 2010 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4              msg match {
     1.5                case XML.Elem(Markup(name, atts), args)
     1.6                if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
     1.7 -                val range = command.decode_range(Position.get_range(atts).get)
     1.8 +                val range = command.decode(Position.get_range(atts).get)
     1.9                  val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    1.10                  val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    1.11                  add_markup(info)
    1.12 @@ -89,7 +89,8 @@
    1.13    val range: Text.Range = Text.Range(0, length)
    1.14  
    1.15    lazy val symbol_index = new Symbol.Index(source)
    1.16 -  def decode_range(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.17 +  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
    1.18 +  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.19  
    1.20  
    1.21    /* accumulated results */