--- a/src/Tools/jEdit/src/document_view.scala Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 14 18:12:41 2012 +0200
@@ -171,7 +171,7 @@
private var control: Boolean = false
- private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.subexp _)
+ private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)