src/Tools/jEdit/src/jedit_rendering.scala
author wenzelm
Mon Mar 11 18:58:06 2019 +0100 (2 months ago ago)
changeset 70079 990c6e8faf2c
parent 69666 c95edf19133b
child 70145 396e0120f7b8
permissions -rw-r--r--
tuned signature;
wenzelm@64623
     1
/*  Title:      Tools/jEdit/src/jedit_rendering.scala
wenzelm@39178
     2
    Author:     Makarius
wenzelm@39178
     3
wenzelm@64623
     4
Isabelle/jEdit-specific implementation of quasi-abstract rendering and
wenzelm@50199
     5
markup interpretation.
wenzelm@39178
     6
*/
wenzelm@39178
     7
wenzelm@39178
     8
package isabelle.jedit
wenzelm@39178
     9
wenzelm@39178
    10
wenzelm@39178
    11
import isabelle._
wenzelm@39178
    12
wenzelm@39178
    13
import java.awt.Color
wenzelm@46227
    14
import javax.swing.Icon
wenzelm@39178
    15
wenzelm@43414
    16
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
wenzelm@61175
    17
import org.gjt.sp.jedit.jEdit
wenzelm@39178
    18
wenzelm@45460
    19
import scala.collection.immutable.SortedMap
wenzelm@45460
    20
wenzelm@39178
    21
wenzelm@64622
    22
object JEdit_Rendering
wenzelm@39178
    23
{
wenzelm@66114
    24
  def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
wenzelm@66114
    25
    new JEdit_Rendering(snapshot, model, options)
wenzelm@39178
    26
wenzelm@49356
    27
wenzelm@53230
    28
  /* popup window bounds */
wenzelm@53230
    29
wenzelm@53230
    30
  def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
wenzelm@53230
    31
wenzelm@53230
    32
wenzelm@55501
    33
  /* Isabelle/Isar token markup */
wenzelm@39179
    34
wenzelm@39179
    35
  private val command_style: Map[String, Byte] =
wenzelm@39179
    36
  {
wenzelm@43414
    37
    import JEditToken._
wenzelm@39179
    38
    Map[String, Byte](
wenzelm@39179
    39
      Keyword.THY_END -> KEYWORD2,
wenzelm@39179
    40
      Keyword.PRF_ASM -> KEYWORD3,
wenzelm@59125
    41
      Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@39179
    42
    ).withDefaultValue(KEYWORD1)
wenzelm@39179
    43
  }
wenzelm@39179
    44
wenzelm@43414
    45
  private val token_style: Map[Token.Kind.Value, Byte] =
wenzelm@39179
    46
  {
wenzelm@43414
    47
    import JEditToken._
wenzelm@43414
    48
    Map[Token.Kind.Value, Byte](
wenzelm@43414
    49
      Token.Kind.KEYWORD -> KEYWORD2,
wenzelm@43414
    50
      Token.Kind.IDENT -> NULL,
wenzelm@43414
    51
      Token.Kind.LONG_IDENT -> NULL,
wenzelm@43414
    52
      Token.Kind.SYM_IDENT -> NULL,
wenzelm@43414
    53
      Token.Kind.VAR -> NULL,
wenzelm@43414
    54
      Token.Kind.TYPE_IDENT -> NULL,
wenzelm@43414
    55
      Token.Kind.TYPE_VAR -> NULL,
wenzelm@43414
    56
      Token.Kind.NAT -> NULL,
wenzelm@43414
    57
      Token.Kind.FLOAT -> NULL,
wenzelm@59081
    58
      Token.Kind.SPACE -> NULL,
wenzelm@43431
    59
      Token.Kind.STRING -> LITERAL1,
wenzelm@43431
    60
      Token.Kind.ALT_STRING -> LITERAL2,
wenzelm@43414
    61
      Token.Kind.VERBATIM -> COMMENT3,
wenzelm@55033
    62
      Token.Kind.CARTOUCHE -> COMMENT4,
wenzelm@67439
    63
      Token.Kind.INFORMAL_COMMENT -> COMMENT1,
wenzelm@67439
    64
      Token.Kind.FORMAL_COMMENT -> COMMENT1,
wenzelm@48754
    65
      Token.Kind.ERROR -> INVALID
wenzelm@39179
    66
    ).withDefaultValue(NULL)
wenzelm@39179
    67
  }
wenzelm@39179
    68
wenzelm@43414
    69
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
wenzelm@63441
    70
    if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
wenzelm@55505
    71
    else if (token.is_delimiter) JEditToken.OPERATOR
wenzelm@43414
    72
    else token_style(token.kind)
wenzelm@55500
    73
wenzelm@55501
    74
wenzelm@55501
    75
  /* Isabelle/ML token markup */
wenzelm@55501
    76
wenzelm@55500
    77
  private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
wenzelm@55500
    78
  {
wenzelm@55500
    79
    import JEditToken._
wenzelm@55500
    80
    Map[ML_Lex.Kind.Value, Byte](
wenzelm@55505
    81
      ML_Lex.Kind.KEYWORD -> NULL,
wenzelm@55500
    82
      ML_Lex.Kind.IDENT -> NULL,
wenzelm@55500
    83
      ML_Lex.Kind.LONG_IDENT -> NULL,
wenzelm@55500
    84
      ML_Lex.Kind.TYPE_VAR -> NULL,
wenzelm@55503
    85
      ML_Lex.Kind.WORD -> DIGIT,
wenzelm@55503
    86
      ML_Lex.Kind.INT -> DIGIT,
wenzelm@55503
    87
      ML_Lex.Kind.REAL -> DIGIT,
wenzelm@55500
    88
      ML_Lex.Kind.CHAR -> LITERAL2,
wenzelm@55500
    89
      ML_Lex.Kind.STRING -> LITERAL1,
wenzelm@55500
    90
      ML_Lex.Kind.SPACE -> NULL,
wenzelm@67438
    91
      ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
wenzelm@67438
    92
      ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
wenzelm@55512
    93
      ML_Lex.Kind.ANTIQ -> NULL,
wenzelm@55512
    94
      ML_Lex.Kind.ANTIQ_START -> LITERAL4,
wenzelm@55512
    95
      ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
wenzelm@55512
    96
      ML_Lex.Kind.ANTIQ_OTHER -> NULL,
wenzelm@55514
    97
      ML_Lex.Kind.ANTIQ_STRING -> NULL,
wenzelm@55514
    98
      ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
wenzelm@55514
    99
      ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
wenzelm@55500
   100
      ML_Lex.Kind.ERROR -> INVALID
wenzelm@55500
   101
    ).withDefaultValue(NULL)
wenzelm@55500
   102
  }
wenzelm@55500
   103
wenzelm@55500
   104
  def ml_token_markup(token: ML_Lex.Token): Byte =
wenzelm@55501
   105
    if (!token.is_keyword) ml_token_style(token.kind)
wenzelm@55505
   106
    else if (token.is_delimiter) JEditToken.OPERATOR
wenzelm@55505
   107
    else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
wenzelm@55505
   108
    else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
wenzelm@55501
   109
    else JEditToken.KEYWORD1
wenzelm@55647
   110
wenzelm@55647
   111
wenzelm@55647
   112
  /* markup elements */
wenzelm@55647
   113
wenzelm@63474
   114
  private val indentation_elements =
wenzelm@63474
   115
    Markup.Elements(Markup.Command_Indent.name)
wenzelm@63474
   116
wenzelm@60878
   117
  private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
wenzelm@60878
   118
wenzelm@55647
   119
  private val highlight_elements =
wenzelm@58545
   120
    Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
wenzelm@69666
   121
      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL,
wenzelm@69661
   122
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
wenzelm@69661
   123
      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
wenzelm@67323
   124
      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
wenzelm@55647
   125
wenzelm@55647
   126
  private val hyperlink_elements =
wenzelm@69666
   127
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.POSITION,
wenzelm@69666
   128
      Markup.CITATION)
wenzelm@55647
   129
wenzelm@55647
   130
  private val gutter_elements =
wenzelm@59203
   131
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
wenzelm@55647
   132
wenzelm@55647
   133
  private val squiggly_elements =
wenzelm@59203
   134
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
wenzelm@55647
   135
wenzelm@55647
   136
  private val line_background_elements =
wenzelm@59184
   137
    Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
wenzelm@59203
   138
      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
wenzelm@59203
   139
      Markup.ERROR_MESSAGE)
wenzelm@55647
   140
wenzelm@55820
   141
  private val separator_elements =
wenzelm@56743
   142
    Markup.Elements(Markup.SEPARATOR)
wenzelm@55647
   143
wenzelm@55820
   144
  private val bullet_elements =
wenzelm@60913
   145
    Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
wenzelm@55647
   146
wenzelm@55647
   147
  private val fold_depth_elements =
wenzelm@56743
   148
    Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
wenzelm@39178
   149
}
wenzelm@49356
   150
wenzelm@49356
   151
wenzelm@66114
   152
class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
wenzelm@65213
   153
  extends Rendering(snapshot, options, PIDE.session)
wenzelm@49356
   154
{
wenzelm@66114
   155
  def model: Document_Model = _model
wenzelm@66114
   156
wenzelm@66114
   157
wenzelm@49356
   158
  /* colors */
wenzelm@49356
   159
wenzelm@65144
   160
  def color(s: String): Color =
wenzelm@65145
   161
    if (s == "main_color") main_color
wenzelm@65144
   162
    else Color_Value(options.string(s))
wenzelm@65144
   163
wenzelm@65144
   164
  def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
wenzelm@49356
   165
wenzelm@65102
   166
  lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
wenzelm@65103
   167
    Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
wenzelm@65102
   168
wenzelm@65145
   169
  val main_color = jEdit.getColorProperty("view.fgColor")
wenzelm@65145
   170
wenzelm@65103
   171
  val outdated_color = color("outdated_color")
wenzelm@65103
   172
  val bullet_color = color("bullet_color")
wenzelm@65103
   173
  val tooltip_color = color("tooltip_color")
wenzelm@65103
   174
  val spell_checker_color = color("spell_checker_color")
wenzelm@65103
   175
  val entity_ref_color = color("entity_ref_color")
wenzelm@65103
   176
  val breakpoint_disabled_color = color("breakpoint_disabled_color")
wenzelm@65103
   177
  val breakpoint_enabled_color = color("breakpoint_enabled_color")
wenzelm@65103
   178
  val caret_debugger_color = color("caret_debugger_color")
wenzelm@65103
   179
  val highlight_color = color("highlight_color")
wenzelm@65103
   180
  val hyperlink_color = color("hyperlink_color")
wenzelm@65103
   181
  val active_hover_color = color("active_hover_color")
wenzelm@65103
   182
  val caret_invisible_color = color("caret_invisible_color")
wenzelm@65103
   183
  val completion_color = color("completion_color")
wenzelm@65103
   184
  val search_color = color("search_color")
wenzelm@49356
   185
wenzelm@49356
   186
wenzelm@63474
   187
  /* indentation */
wenzelm@63474
   188
wenzelm@63474
   189
  def indentation(range: Text.Range): Int =
wenzelm@64622
   190
    snapshot.select(range, JEdit_Rendering.indentation_elements, _ =>
wenzelm@63474
   191
      {
wenzelm@63474
   192
        case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
wenzelm@63474
   193
        case _ => None
wenzelm@63474
   194
      }).headOption.map(_.info).getOrElse(0)
wenzelm@63474
   195
wenzelm@63474
   196
wenzelm@60878
   197
  /* breakpoints */
wenzelm@60878
   198
wenzelm@60880
   199
  def breakpoint(range: Text.Range): Option[(Command, Long)] =
wenzelm@60880
   200
    if (snapshot.is_outdated) None
wenzelm@60880
   201
    else
wenzelm@64622
   202
      snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states =>
wenzelm@60880
   203
        {
wenzelm@60882
   204
          case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
wenzelm@60880
   205
            command_states match {
wenzelm@60882
   206
              case st :: _ => Some((st.command, breakpoint))
wenzelm@60880
   207
              case _ => None
wenzelm@60880
   208
            }
wenzelm@60880
   209
          case _ => None
wenzelm@60880
   210
        }).headOption.map(_.info)
wenzelm@60878
   211
wenzelm@60878
   212
wenzelm@62986
   213
  /* caret focus */
wenzelm@62986
   214
wenzelm@62991
   215
  def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
wenzelm@64767
   216
    snapshot.select(range, Rendering.caret_focus_elements, _ =>
wenzelm@62988
   217
      {
wenzelm@62991
   218
        case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
wenzelm@62991
   219
          Some(entity_ref_color)
wenzelm@62988
   220
        case _ => None
wenzelm@62988
   221
      })
wenzelm@62988
   222
wenzelm@62986
   223
wenzelm@55626
   224
  /* highlighted area */
wenzelm@49356
   225
wenzelm@49358
   226
  def highlight(range: Text.Range): Option[Text.Info[Color]] =
wenzelm@64622
   227
    snapshot.select(range, JEdit_Rendering.highlight_elements, _ =>
wenzelm@55620
   228
      {
wenzelm@55620
   229
        case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
wenzelm@55689
   230
      }).headOption.map(_.info)
wenzelm@49356
   231
wenzelm@49356
   232
wenzelm@55626
   233
  /* hyperlinks */
wenzelm@55626
   234
wenzelm@66082
   235
  def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
wenzelm@49356
   236
  {
wenzelm@66082
   237
    snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
wenzelm@64622
   238
      range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
wenzelm@49356
   239
        {
wenzelm@56458
   240
          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
wenzelm@65488
   241
            val file = perhaps_append_file(snapshot.node_name, name)
wenzelm@66082
   242
            val link = PIDE.editor.hyperlink_file(true, file)
wenzelm@55622
   243
            Some(links :+ Text.Info(snapshot.convert(info_range), link))
wenzelm@49356
   244
wenzelm@61660
   245
          case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
wenzelm@66082
   246
            PIDE.editor.hyperlink_doc(name).map(link =>
wenzelm@61660
   247
              (links :+ Text.Info(snapshot.convert(info_range), link)))
wenzelm@61660
   248
wenzelm@54702
   249
          case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
wenzelm@66082
   250
            val link = PIDE.editor.hyperlink_url(name)
wenzelm@55622
   251
            Some(links :+ Text.Info(snapshot.convert(info_range), link))
wenzelm@54702
   252
wenzelm@64660
   253
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@66082
   254
            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
wenzelm@60215
   255
            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
wenzelm@49356
   256
wenzelm@55547
   257
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@66082
   258
            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
wenzelm@60215
   259
            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
wenzelm@52889
   260
wenzelm@58545
   261
          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
wenzelm@58545
   262
            val opt_link =
wenzelm@66150
   263
              Document_Model.bibtex_entries_iterator().collectFirst(
wenzelm@64831
   264
                { case Text.Info(entry_range, (entry, model)) if entry == name =>
wenzelm@66082
   265
                    PIDE.editor.hyperlink_model(true, model, entry_range.start) })
wenzelm@60215
   266
            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
wenzelm@58545
   267
wenzelm@52889
   268
          case _ => None
wenzelm@55622
   269
        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
wenzelm@49356
   270
  }
wenzelm@49356
   271
wenzelm@49356
   272
wenzelm@55626
   273
  /* active elements */
wenzelm@55626
   274
wenzelm@50450
   275
  def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
wenzelm@65102
   276
    snapshot.select(range, Rendering.active_elements, command_states =>
wenzelm@55620
   277
      {
wenzelm@55620
   278
        case Text.Info(info_range, elem) =>
wenzelm@55623
   279
          if (elem.name == Markup.DIALOG) {
wenzelm@55623
   280
            elem match {
wenzelm@55623
   281
              case Protocol.Dialog(_, serial, _)
wenzelm@56354
   282
              if !command_states.exists(st => st.results.defined(serial)) =>
wenzelm@55623
   283
                Some(Text.Info(snapshot.convert(info_range), elem))
wenzelm@55623
   284
              case _ => None
wenzelm@55623
   285
            }
wenzelm@55623
   286
          }
wenzelm@55623
   287
          else Some(Text.Info(snapshot.convert(info_range), elem))
wenzelm@55689
   288
      }).headOption.map(_.info)
wenzelm@49492
   289
wenzelm@55626
   290
wenzelm@55626
   291
  /* tooltips */
wenzelm@55626
   292
wenzelm@55647
   293
  def tooltip_margin: Int = options.int("jedit_tooltip_margin")
wenzelm@70079
   294
  override def timing_threshold: Double = options.real("jedit_timing_threshold")
wenzelm@50554
   295
wenzelm@64748
   296
  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
wenzelm@65132
   297
    tooltips(Rendering.tooltip_elements, range).map(info => info.map(Pretty.fbreaks(_)))
wenzelm@65129
   298
wenzelm@65129
   299
  def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
wenzelm@65132
   300
    tooltips(Rendering.tooltip_message_elements, range).map(info => info.map(Pretty.fbreaks(_)))
wenzelm@64748
   301
wenzelm@52873
   302
  lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
wenzelm@52873
   303
  lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
wenzelm@52472
   304
wenzelm@52472
   305
wenzelm@56495
   306
  /* gutter */
wenzelm@56495
   307
wenzelm@56495
   308
  private def gutter_message_pri(msg: XML.Tree): Int =
wenzelm@64676
   309
    if (Protocol.is_error(msg)) Rendering.error_pri
wenzelm@64676
   310
    else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
wenzelm@64676
   311
    else if (Protocol.is_warning(msg)) Rendering.warning_pri
wenzelm@64676
   312
    else if (Protocol.is_information(msg)) Rendering.information_pri
wenzelm@56495
   313
    else 0
wenzelm@55626
   314
wenzelm@59129
   315
  private lazy val gutter_message_content = Map(
wenzelm@64676
   316
    Rendering.information_pri ->
wenzelm@65127
   317
      (JEdit_Lib.load_icon(options.string("gutter_information_icon")),
wenzelm@65127
   318
        color(Rendering.Color.information_message)),
wenzelm@64676
   319
    Rendering.warning_pri ->
wenzelm@65127
   320
      (JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
wenzelm@65127
   321
        color(Rendering.Color.warning_message)),
wenzelm@64676
   322
    Rendering.legacy_pri ->
wenzelm@65127
   323
      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
wenzelm@65127
   324
        color(Rendering.Color.legacy_message)),
wenzelm@64676
   325
    Rendering.error_pri ->
wenzelm@65127
   326
      (JEdit_Lib.load_icon(options.string("gutter_error_icon")),
wenzelm@65127
   327
        color(Rendering.Color.error_message)))
wenzelm@49356
   328
wenzelm@59129
   329
  def gutter_content(range: Text.Range): Option[(Icon, Color)] =
wenzelm@49356
   330
  {
wenzelm@56495
   331
    val pris =
wenzelm@64622
   332
      snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
wenzelm@49356
   333
        {
wenzelm@56495
   334
          case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
wenzelm@56495
   335
            Some(pri max gutter_message_pri(msg))
wenzelm@52889
   336
          case _ => None
wenzelm@56495
   337
        }).map(_.info)
wenzelm@56495
   338
wenzelm@59129
   339
    gutter_message_content.get((0 /: pris)(_ max _))
wenzelm@49356
   340
  }
wenzelm@49356
   341
wenzelm@49356
   342
wenzelm@65128
   343
  /* message output */
wenzelm@55626
   344
wenzelm@65121
   345
  def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65121
   346
    message_underline_color(JEdit_Rendering.squiggly_elements, range)
wenzelm@49356
   347
wenzelm@65124
   348
  def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
wenzelm@49473
   349
  {
wenzelm@49474
   350
    val results =
wenzelm@64622
   351
      snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
wenzelm@49473
   352
        {
wenzelm@64676
   353
          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
wenzelm@49474
   354
        })
wenzelm@49474
   355
    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
wenzelm@49474
   356
wenzelm@65124
   357
    Rendering.message_background_color.get(pri).map(message_color =>
wenzelm@61719
   358
      {
wenzelm@61719
   359
        val is_separator =
wenzelm@64622
   360
          snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
wenzelm@61719
   361
            {
wenzelm@61719
   362
              case _ => Some(true)
wenzelm@61719
   363
            }).exists(_.info)
wenzelm@61719
   364
        (message_color, is_separator)
wenzelm@61719
   365
      })
wenzelm@49473
   366
  }
wenzelm@49356
   367
wenzelm@50500
   368
wenzelm@55626
   369
  /* text color */
wenzelm@55626
   370
wenzelm@65144
   371
  def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] =
wenzelm@49356
   372
  {
wenzelm@65258
   373
    if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color))
wenzelm@50196
   374
    else
wenzelm@65144
   375
      snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
wenzelm@50196
   376
        {
wenzelm@65144
   377
          case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color(_))
wenzelm@50196
   378
        })
wenzelm@49356
   379
  }
wenzelm@50542
   380
wenzelm@50542
   381
wenzelm@55626
   382
  /* virtual bullets */
wenzelm@55626
   383
wenzelm@55626
   384
  def bullet(range: Text.Range): List[Text.Info[Color]] =
wenzelm@64622
   385
    snapshot.select(range, JEdit_Rendering.bullet_elements, _ =>
wenzelm@60913
   386
      {
wenzelm@60913
   387
        case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
wenzelm@65247
   388
          PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b =>
wenzelm@60913
   389
            if (b) breakpoint_enabled_color else breakpoint_disabled_color)
wenzelm@60913
   390
        case _ => Some(bullet_color)
wenzelm@60913
   391
      })
wenzelm@55626
   392
wenzelm@55626
   393
wenzelm@55626
   394
  /* text folds */
wenzelm@50542
   395
wenzelm@52900
   396
  def fold_depth(range: Text.Range): List[Text.Info[Int]] =
wenzelm@64622
   397
    snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ =>
wenzelm@50542
   398
      {
wenzelm@55620
   399
        case (depth, _) => Some(depth + 1)
wenzelm@50542
   400
      })
wenzelm@49356
   401
}