src/Tools/jEdit/src/isabelle_rendering.scala
changeset 49674 dbadb4d03cbc
parent 49554 7b7bd2d7661d
child 49700 2d1cbdf6a68b
     1.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Oct 01 12:05:05 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Oct 01 16:37:22 2012 +0200
     1.3 @@ -181,9 +181,9 @@
     1.4    private val highlight_include =
     1.5      Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
     1.6        Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
     1.7 -      Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
     1.8 -      Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
     1.9 -      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
    1.10 +      Isabelle_Markup.PATH, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.FREE,
    1.11 +      Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE,
    1.12 +      Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
    1.13  
    1.14    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    1.15    {
    1.16 @@ -299,8 +299,8 @@
    1.17        Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
    1.18  
    1.19    private val tooltip_elements =
    1.20 -    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
    1.21 -      Isabelle_Markup.PATH) ++ tooltips.keys
    1.22 +    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING,
    1.23 +      Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys
    1.24  
    1.25    private def string_of_typing(kind: String, body: XML.Body): String =
    1.26      Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
    1.27 @@ -322,7 +322,8 @@
    1.28            if Path.is_ok(name) =>
    1.29              val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    1.30              add(prev, r, (true, "file " + quote(jedit_file)))
    1.31 -          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
    1.32 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    1.33 +          if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING =>
    1.34              add(prev, r, (true, string_of_typing("::", body)))
    1.35            case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
    1.36              add(prev, r, (false, string_of_typing("ML:", body)))