src/Tools/jEdit/src/rendering.scala
changeset 55552 bcc643ac071a
parent 55547 4a9f76263ece
child 55615 bf4bbe72f740
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 18 15:38:50 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 18 16:34:02 2014 +0100
     1.3 @@ -241,10 +241,10 @@
     1.4    /* markup selectors */
     1.5  
     1.6    private val highlight_include =
     1.7 -    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
     1.8 -      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE,
     1.9 -      Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE,
    1.10 -      Markup.DOCUMENT_SOURCE)
    1.11 +    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    1.12 +      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    1.13 +      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    1.14 +      Markup.VAR, Markup.TFREE, Markup.TVAR)
    1.15  
    1.16    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    1.17    {
    1.18 @@ -375,23 +375,18 @@
    1.19  
    1.20    private val tooltips: Map[String, String] =
    1.21      Map(
    1.22 -      Markup.SORT -> "sort",
    1.23 -      Markup.TYP -> "type",
    1.24 -      Markup.TERM -> "term",
    1.25 -      Markup.PROP -> "proposition",
    1.26        Markup.TOKEN_RANGE -> "inner syntax token",
    1.27        Markup.FREE -> "free variable",
    1.28        Markup.SKOLEM -> "skolem variable",
    1.29        Markup.BOUND -> "bound variable",
    1.30        Markup.VAR -> "schematic variable",
    1.31        Markup.TFREE -> "free type variable",
    1.32 -      Markup.TVAR -> "schematic type variable",
    1.33 -      Markup.ML_SOURCE -> "ML source",
    1.34 -      Markup.DOCUMENT_SOURCE -> "document source")
    1.35 +      Markup.TVAR -> "schematic type variable")
    1.36  
    1.37    private val tooltip_elements =
    1.38 -    Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
    1.39 -      Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys
    1.40 +    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    1.41 +      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    1.42 +      tooltips.keys
    1.43  
    1.44    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.45      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    1.46 @@ -434,6 +429,8 @@
    1.47              Some(add(prev, r, (true, pretty_typing("::", body))))
    1.48            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    1.49              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    1.50 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) =>
    1.51 +            Some(add(prev, r, (true, XML.Text("language: " + name))))
    1.52            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    1.53              if (tooltips.isDefinedAt(name))
    1.54                Some(add(prev, r, (true, XML.Text(tooltips(name)))))