src/Tools/jEdit/src/isabelle_rendering.scala

   /* markup selectors */
 
   private val highlight_include =
     Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
       Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
-      Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
-      Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
-      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
+      Isabelle_Markup.PATH, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.FREE,
+      Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE,
+      Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
     snapshot.select_markup(range, Some(highlight_include),
         {

       Isabelle_Markup.TVAR -> "schematic type variable",
       Isabelle_Markup.ML_SOURCE -> "ML source",
       Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
 
   private val tooltip_elements =
-    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
-      Isabelle_Markup.PATH) ++ tooltips.keys
+    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
+      Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
 
   private def string_of_typing(kind: String, body: XML.Body): String =
     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
       margin = options.int("jedit_tooltip_margin"))
 

             add(prev, r, (true, kind1 + " " + quote(name)))
           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
             add(prev, r, (true, "file " + quote(jedit_file)))
-          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
+          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
+          if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
             add(prev, r, (true, string_of_typing("::", body)))
           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
             add(prev, r, (false, string_of_typing("ML:", body)))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
           if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))