1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 14:36:17 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 15:15:41 2014 +0100
     1.3 @@ -230,7 +230,8 @@
     1.4  
     1.5    val overview_limit = options.int("jedit_text_overview_limit")
     1.6  
     1.7 -  private val overview_include = Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
     1.8 +  private val overview_elements =
     1.9 +    Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
    1.10  
    1.11    def overview_color(range: Text.Range): Option[Color] =
    1.12    {
    1.13 @@ -238,12 +239,12 @@
    1.14      else {
    1.15        val results =
    1.16          snapshot.cumulate_markup[(Protocol.Status, Int)](
    1.17 -          range, (Protocol.Status.init, 0), Some(overview_include), _ =>
    1.18 +          range, (Protocol.Status.init, 0), Some(overview_elements), _ =>
    1.19            {
    1.20              case ((status, pri), Text.Info(_, elem)) =>
    1.21                if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
    1.22                  Some((status, pri max Rendering.message_pri(elem.name)))
    1.23 -              else if (overview_include(elem.name))
    1.24 +              else if (overview_elements(elem.name))
    1.25                  Some((Protocol.command_status(status, elem.markup), pri))
    1.26                else None
    1.27            })
    1.28 @@ -266,7 +267,7 @@
    1.29  
    1.30    /* markup selectors */
    1.31  
    1.32 -  private val highlight_include =
    1.33 +  private val highlight_elements =
    1.34      Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    1.35        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    1.36        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    1.37 @@ -274,17 +275,18 @@
    1.38  
    1.39    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    1.40    {
    1.41 -    snapshot.select_markup(range, Some(highlight_include), _ =>
    1.42 +    snapshot.select_markup(range, Some(highlight_elements), _ =>
    1.43          {
    1.44            case Text.Info(info_range, elem) =>
    1.45 -            if (highlight_include(elem.name))
    1.46 +            if (highlight_elements(elem.name))
    1.47                Some(Text.Info(snapshot.convert(info_range), highlight_color))
    1.48              else None
    1.49          }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.50    }
    1.51  
    1.52  
    1.53 -  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    1.54 +  private val hyperlink_elements =
    1.55 +    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    1.56  
    1.57    private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
    1.58      if (Path.is_ok(name))
    1.59 @@ -303,7 +305,7 @@
    1.60    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.61    {
    1.62      snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
    1.63 -      range, Nil, Some(hyperlink_include), _ =>
    1.64 +      range, Nil, Some(hyperlink_elements), _ =>
    1.65          {
    1.66            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    1.67            if Path.is_ok(name) =>
    1.68 @@ -343,11 +345,11 @@
    1.69    }
    1.70  
    1.71  
    1.72 -  private val active_include =
    1.73 +  private val active_elements =
    1.74      Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
    1.75  
    1.76    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    1.77 -    snapshot.select_markup(range, Some(active_include), command_state =>
    1.78 +    snapshot.select_markup(range, Some(active_elements), command_state =>
    1.79          {
    1.80            case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    1.81            if !command_state.results.defined(serial) =>
    1.82 @@ -516,17 +518,17 @@
    1.83      Rendering.warning_pri -> warning_color,
    1.84      Rendering.error_pri -> error_color)
    1.85  
    1.86 -  private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.87 +  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.88  
    1.89    def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
    1.90    {
    1.91      val results =
    1.92 -      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
    1.93 +      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
    1.94          {
    1.95            case (pri, Text.Info(_, elem)) =>
    1.96              if (Protocol.is_information(elem))
    1.97                Some(pri max Rendering.information_pri)
    1.98 -            else if (squiggly_include.contains(elem.name))
    1.99 +            else if (squiggly_elements(elem.name))
   1.100                Some(pri max Rendering.message_pri(elem.name))
   1.101              else None
   1.102          })
   1.103 @@ -579,10 +581,10 @@
   1.104      st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
   1.105  
   1.106  
   1.107 -  private val background1_include =
   1.108 +  private val background1_elements =
   1.109      Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
   1.110        Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
   1.111 -      active_include
   1.112 +      active_elements
   1.113  
   1.114    def background1(range: Text.Range): List[Text.Info[Color]] =
   1.115    {
   1.116 @@ -591,7 +593,7 @@
   1.117        for {
   1.118          Text.Info(r, result) <-
   1.119            snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   1.120 -            range, (Some(Protocol.Status.init), None), Some(background1_include), command_state =>
   1.121 +            range, (Some(Protocol.Status.init), None), Some(background1_elements), command_state =>
   1.122              {
   1.123                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   1.124                if (Protocol.command_status_markup(markup.name)) =>
   1.125 @@ -608,7 +610,7 @@
   1.126                      Some((None, Some(active_color)))
   1.127                  }
   1.128                case (_, Text.Info(_, elem)) =>
   1.129 -                if (active_include(elem.name)) Some((None, Some(active_color)))
   1.130 +                if (active_elements(elem.name)) Some((None, Some(active_color)))
   1.131                  else None
   1.132              })
   1.133          color <-
   1.134 @@ -639,15 +641,15 @@
   1.135        })
   1.136  
   1.137  
   1.138 -  private val foreground_include =
   1.139 +  private val foreground_elements =
   1.140      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
   1.141  
   1.142    def foreground(range: Text.Range): List[Text.Info[Color]] =
   1.143 -    snapshot.select_markup(range, Some(foreground_include), _ =>
   1.144 +    snapshot.select_markup(range, Some(foreground_elements), _ =>
   1.145        {
   1.146          case Text.Info(_, elem) =>
   1.147            if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
   1.148 -          else if (foreground_include.contains(elem.name)) Some(quoted_color)
   1.149 +          else if (foreground_elements(elem.name)) Some(quoted_color)
   1.150            else None
   1.151        })
   1.152  
   1.153 @@ -696,12 +698,12 @@
   1.154  
   1.155    /* nested text structure -- folds */
   1.156  
   1.157 -  private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   1.158 +  private val fold_depth_elements = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   1.159  
   1.160    def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   1.161 -    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
   1.162 +    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_elements), _ =>
   1.163        {
   1.164          case (depth, Text.Info(_, elem)) =>
   1.165 -          if (fold_depth_include(elem.name)) Some(depth + 1) else None
   1.166 +          if (fold_depth_elements(elem.name)) Some(depth + 1) else None
   1.167        })
   1.168  }