--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Nov 22 13:21:02 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Nov 22 14:40:39 2012 +0100
@@ -136,7 +136,7 @@
private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
private val sendback_area =
- new Active_Area[Document.Exec_ID]((r: Isabelle_Rendering) => r.sendback _)
+ new Active_Area[Option[Document.Exec_ID]]((r: Isabelle_Rendering) => r.sendback _)
private val active_areas =
List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))