src/Tools/jEdit/src/isabelle_markup.scala
changeset 45474 f793dd5d84b2
parent 45468 33e946d3f449
child 45489 9b6f55f34b70
     1.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 18:56:49 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 19:44:56 2011 +0100
     1.3 @@ -89,11 +89,12 @@
     1.4  
     1.5    val message =
     1.6      Markup_Tree.Select[Color](
     1.7 -    {
     1.8 -      case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
     1.9 -      case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    1.10 -      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    1.11 -    })
    1.12 +      {
    1.13 +        case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    1.14 +        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    1.15 +        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    1.16 +      },
    1.17 +      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
    1.18  
    1.19    val tooltip_message =
    1.20      Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
    1.21 @@ -102,7 +103,8 @@
    1.22          if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
    1.23            msgs + (serial ->
    1.24              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    1.25 -      })
    1.26 +      },
    1.27 +      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
    1.28  
    1.29    val gutter_message =
    1.30      Markup_Tree.Select[Icon](
    1.31 @@ -113,20 +115,23 @@
    1.32              case _ => warning_icon
    1.33            }
    1.34          case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    1.35 -      })
    1.36 +      },
    1.37 +      Some(Set(Markup.WARNING, Markup.ERROR)))
    1.38  
    1.39    val background1 =
    1.40      Markup_Tree.Select[Color](
    1.41        {
    1.42          case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    1.43          case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
    1.44 -      })
    1.45 +      },
    1.46 +      Some(Set(Markup.BAD, Markup.HILITE)))
    1.47  
    1.48    val background2 =
    1.49      Markup_Tree.Select[Color](
    1.50        {
    1.51          case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    1.52 -      })
    1.53 +      },
    1.54 +      Some(Set(Markup.TOKEN_RANGE)))
    1.55  
    1.56    val foreground =
    1.57      Markup_Tree.Select[Color](
    1.58 @@ -134,7 +139,8 @@
    1.59          case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
    1.60          case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
    1.61          case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
    1.62 -      })
    1.63 +      },
    1.64 +      Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
    1.65  
    1.66    private val text_colors: Map[String, Color] =
    1.67      Map(
    1.68 @@ -164,8 +170,10 @@
    1.69    val text_color =
    1.70      Markup_Tree.Select[Color](
    1.71        {
    1.72 -        case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
    1.73 -      })
    1.74 +        case Text.Info(_, XML.Elem(Markup(m, _), _))
    1.75 +        if text_colors.isDefinedAt(m) => text_colors(m)
    1.76 +      },
    1.77 +      Some(Set() ++ text_colors.keys))
    1.78  
    1.79    private val tooltips: Map[String, String] =
    1.80      Map(
    1.81 @@ -191,16 +199,19 @@
    1.82      Markup_Tree.Select[String](
    1.83        {
    1.84          case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
    1.85 -        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
    1.86 +        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    1.87 +          string_of_typing("ML:", body)
    1.88          case Text.Info(_, XML.Elem(Markup(name, _), _))
    1.89          if tooltips.isDefinedAt(name) => tooltips(name)
    1.90 -      })
    1.91 +      },
    1.92 +      Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
    1.93  
    1.94    val tooltip2 =
    1.95      Markup_Tree.Select[String](
    1.96        {
    1.97          case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
    1.98 -      })
    1.99 +      },
   1.100 +      Some(Set(Markup.TYPING)))
   1.101  
   1.102    private val subexp_include =
   1.103      Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   1.104 @@ -212,7 +223,8 @@
   1.105        {
   1.106          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   1.107            (range, subexp_color)
   1.108 -      })
   1.109 +      },
   1.110 +      Some(subexp_include))
   1.111  
   1.112  
   1.113    /* token markup -- text styles */