src/Tools/jEdit/src/rich_text_area.scala
changeset 50215 97959912840a
parent 50211 2a3d6d760629
child 50216 de77cde57376
     1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
     1.3 @@ -134,7 +134,7 @@
     1.4  
     1.5    private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
     1.6    private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
     1.7 -  private val sendback_area = new Active_Area[Option[Document.Exec_ID]]((r: Rendering) => r.sendback _)
     1.8 +  private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
     1.9  
    1.10    private val active_areas =
    1.11      List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
    1.12 @@ -157,7 +157,7 @@
    1.13            case None =>
    1.14          }
    1.15          sendback_area.text_info match {
    1.16 -          case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id)
    1.17 +          case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
    1.18            case None =>
    1.19          }
    1.20        }