src/Tools/jEdit/src/rendering.scala
changeset 55820 61869776ce1f
parent 55790 4670f18baba5
child 55823 0331b6d2ab0c
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 09:34:08 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 12:07:26 2014 +0100
     1.3 @@ -150,28 +150,29 @@
     1.4  
     1.5    /* markup elements */
     1.6  
     1.7 -  private val completion_names_elements = Set(Markup.COMPLETION)
     1.8 +  private val completion_names_elements =
     1.9 +    Document.Elements(Markup.COMPLETION)
    1.10  
    1.11    private val language_context_elements =
    1.12 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.13 +    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.14        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
    1.15        Markup.ML_STRING, Markup.ML_COMMENT)
    1.16  
    1.17    private val highlight_elements =
    1.18 -    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    1.19 +    Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    1.20        Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
    1.21        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
    1.22        Markup.VAR, Markup.TFREE, Markup.TVAR)
    1.23  
    1.24    private val hyperlink_elements =
    1.25 -    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    1.26 +    Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    1.27  
    1.28    private val active_elements =
    1.29 -    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.30 +    Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.31        Markup.SENDBACK, Markup.SIMP_TRACE)
    1.32  
    1.33    private val tooltip_message_elements =
    1.34 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    1.35 +    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    1.36  
    1.37    private val tooltip_descriptions =
    1.38      Map(
    1.39 @@ -184,22 +185,23 @@
    1.40        Markup.TVAR -> "schematic type variable")
    1.41  
    1.42    private val tooltip_elements =
    1.43 -    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    1.44 +    Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    1.45        Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    1.46 -      tooltip_descriptions.keys
    1.47 +    Document.Elements(tooltip_descriptions.keySet)
    1.48  
    1.49    private val gutter_elements =
    1.50 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.51 +    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.52  
    1.53    private val squiggly_elements =
    1.54 -    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.55 +    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.56  
    1.57    private val line_background_elements =
    1.58 -    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    1.59 +    Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
    1.60        Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
    1.61        Markup.INFORMATION)
    1.62  
    1.63 -  private val separator_elements = Set(Markup.SEPARATOR)
    1.64 +  private val separator_elements =
    1.65 +    Document.Elements(Markup.SEPARATOR)
    1.66  
    1.67    private val background_elements =
    1.68      Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
    1.69 @@ -208,13 +210,14 @@
    1.70        active_elements
    1.71  
    1.72    private val foreground_elements =
    1.73 -    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.74 +    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.75        Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.76  
    1.77 -  private val bullet_elements = Set(Markup.BULLET)
    1.78 +  private val bullet_elements =
    1.79 +    Document.Elements(Markup.BULLET)
    1.80  
    1.81    private val fold_depth_elements =
    1.82 -    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    1.83 +    Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
    1.84  }
    1.85  
    1.86  
    1.87 @@ -421,7 +424,7 @@
    1.88    def command_results(range: Text.Range): Command.Results =
    1.89    {
    1.90      val results =
    1.91 -      snapshot.select[Command.Results](range, _ => true, command_state =>
    1.92 +      snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
    1.93          { case _ => Some(command_state.results) }).map(_.info)
    1.94      (Command.Results.empty /: results)(_ ++ _)
    1.95    }
    1.96 @@ -703,7 +706,8 @@
    1.97        Markup.ML_STRING -> inner_quoted_color,
    1.98        Markup.ML_COMMENT -> inner_comment_color)
    1.99  
   1.100 -  private lazy val text_color_elements = text_colors.keySet
   1.101 +  private lazy val text_color_elements =
   1.102 +    Document.Elements(text_colors.keySet)
   1.103  
   1.104    def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   1.105    {