src/Tools/jEdit/src/rendering.scala
changeset 50215 97959912840a
parent 50206 6626bc5ed053
child 50450 358b6020f8b6
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 16:16:47 2012 +0100
     1.3 @@ -249,11 +249,11 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
     1.8 +  def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
     1.9      snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
    1.10          {
    1.11            case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
    1.12 -            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
    1.13 +            Text.Info(snapshot.convert(info_range), props)
    1.14          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    1.15  
    1.16