# HG changeset patch
# User wenzelm
# Date 1349951858 -7200
# Node ID e4f87bd5f22346b2e6791fe1c5b5236094314ca7
# Parent  0aaed83532e1f4e52ee6967a9990ec7c23c290ad
tuned;

diff -r 0aaed83532e1 -r e4f87bd5f223 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Oct 11 00:13:21 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Oct 11 12:37:38 2012 +0200
@@ -211,10 +211,10 @@
             Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
-          if (props.find(
+          if !props.exists(
             { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
               case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
-              case _ => false }).isEmpty) =>
+              case _ => false }) =>
 
             props match {
               case Position.Def_Line_File(line, name) if Path.is_ok(name) =>