1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 15 21:42:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 15 22:48:56 2010 +0200
     1.3 @@ -64,12 +64,12 @@
     1.4          case Command.TypeInfo(_) => true
     1.5          case _ => false }).flatten
     1.6  
     1.7 -    def type_at(pos: Int): Option[String] =
     1.8 +    def type_at(pos: Text.Offset): Option[String] =
     1.9      {
    1.10 -      types.find(t => t.start <= pos && pos < t.stop) match {
    1.11 +      types.find(t => t.range.start <= pos && pos < t.range.stop) match {
    1.12          case Some(t) =>
    1.13            t.info match {
    1.14 -            case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
    1.15 +            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    1.16              case _ => None
    1.17            }
    1.18          case None => None
    1.19 @@ -81,8 +81,8 @@
    1.20          case Command.RefInfo(_, _, _, _) => true
    1.21          case _ => false }).flatten
    1.22  
    1.23 -    def ref_at(pos: Int): Option[Markup_Node] =
    1.24 -      refs.find(t => t.start <= pos && pos < t.stop)
    1.25 +    def ref_at(pos: Text.Offset): Option[Markup_Node] =
    1.26 +      refs.find(t => t.range.start <= pos && pos < t.range.stop)
    1.27  
    1.28  
    1.29      /* message dispatch */
    1.30 @@ -166,7 +166,7 @@
    1.31    /* source text */
    1.32  
    1.33    val source: String = span.map(_.source).mkString
    1.34 -  def source(i: Int, j: Int): String = source.substring(i, j)
    1.35 +  def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.36    def length: Int = source.length
    1.37  
    1.38    lazy val symbol_index = new Symbol.Index(source)
    1.39 @@ -178,7 +178,7 @@
    1.40    {
    1.41      val start = symbol_index.decode(begin)
    1.42      val stop = symbol_index.decode(end)
    1.43 -    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
    1.44 +    new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
    1.45    }
    1.46  
    1.47