symbolic Rendering.Color;
authorwenzelm
Sat Mar 04 09:27:51 2017 +0100 (2017-03-04)
changeset 651014263b2a201b3
parent 65100 83d1f210a1d3
child 65102 136b620b11af
symbolic Rendering.Color;
clarified modules;
src/Pure/PIDE/rendering.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/jedit_rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Sat Mar 04 08:41:32 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Sat Mar 04 09:27:51 2017 +0100
     1.3 @@ -10,6 +10,26 @@
     1.4  
     1.5  object Rendering
     1.6  {
     1.7 +  /* color */
     1.8 +
     1.9 +  object Color extends Enumeration
    1.10 +  {
    1.11 +    val unprocessed1 = Value("unprocessed1")
    1.12 +    val running1 = Value("running1")
    1.13 +    val bad = Value("bad")
    1.14 +    val intensify = Value("intensify")
    1.15 +    val entity = Value("entity")
    1.16 +    val quoted = Value("quoted")
    1.17 +    val antiquoted = Value("antiquoted")
    1.18 +    val active = Value("active")
    1.19 +    val active_result = Value("active_result")
    1.20 +    val markdown_item1 = Value("markdown_item1")
    1.21 +    val markdown_item2 = Value("markdown_item2")
    1.22 +    val markdown_item3 = Value("markdown_item3")
    1.23 +    val markdown_item4 = Value("markdown_item4")
    1.24 +  }
    1.25 +
    1.26 +
    1.27    /* message priorities */
    1.28  
    1.29    val state_pri = 1
    1.30 @@ -39,6 +59,22 @@
    1.31  
    1.32    /* markup elements */
    1.33  
    1.34 +  val active_elements =
    1.35 +    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    1.36 +      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
    1.37 +
    1.38 +  private val background_elements =
    1.39 +    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    1.40 +      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    1.41 +      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    1.42 +      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    1.43 +      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    1.44 +      Markup.Markdown_Item.name ++ active_elements
    1.45 +
    1.46 +  private val foreground_elements =
    1.47 +    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    1.48 +      Markup.CARTOUCHE, Markup.ANTIQUOTED)
    1.49 +
    1.50    private val semantic_completion_elements =
    1.51      Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    1.52  
    1.53 @@ -187,6 +223,76 @@
    1.54    }
    1.55  
    1.56  
    1.57 +  /* text background */
    1.58 +
    1.59 +  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
    1.60 +  {
    1.61 +    for {
    1.62 +      Text.Info(r, result) <-
    1.63 +        snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
    1.64 +          range, (List(Markup.Empty), None), Rendering.background_elements,
    1.65 +          command_states =>
    1.66 +            {
    1.67 +              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
    1.68 +              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
    1.69 +                Some((markup :: markups, color))
    1.70 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
    1.71 +                Some((Nil, Some(Rendering.Color.bad)))
    1.72 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    1.73 +                Some((Nil, Some(Rendering.Color.intensify)))
    1.74 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.75 +                props match {
    1.76 +                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
    1.77 +                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
    1.78 +                  case _ => None
    1.79 +                }
    1.80 +              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
    1.81 +                val color =
    1.82 +                  depth match {
    1.83 +                    case 1 => Rendering.Color.markdown_item1
    1.84 +                    case 2 => Rendering.Color.markdown_item2
    1.85 +                    case 3 => Rendering.Color.markdown_item3
    1.86 +                    case _ => Rendering.Color.markdown_item4
    1.87 +                  }
    1.88 +                Some((Nil, Some(color)))
    1.89 +              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    1.90 +                command_states.collectFirst(
    1.91 +                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
    1.92 +                {
    1.93 +                  case Some(Protocol.Dialog_Result(res)) if res == result =>
    1.94 +                    Some((Nil, Some(Rendering.Color.active_result)))
    1.95 +                  case _ =>
    1.96 +                    Some((Nil, Some(Rendering.Color.active)))
    1.97 +                }
    1.98 +              case (_, Text.Info(_, elem)) =>
    1.99 +                if (Rendering.active_elements(elem.name))
   1.100 +                  Some((Nil, Some(Rendering.Color.active)))
   1.101 +                else None
   1.102 +            })
   1.103 +      color <-
   1.104 +        (result match {
   1.105 +          case (markups, opt_color) if markups.nonEmpty =>
   1.106 +            val status = Protocol.Status.make(markups.iterator)
   1.107 +            if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
   1.108 +            else if (status.is_running) Some(Rendering.Color.running1)
   1.109 +            else opt_color
   1.110 +          case (_, opt_color) => opt_color
   1.111 +        })
   1.112 +    } yield Text.Info(r, color)
   1.113 +  }
   1.114 +
   1.115 +
   1.116 +  /* text foreground */
   1.117 +
   1.118 +  def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
   1.119 +    snapshot.select(range, Rendering.foreground_elements, _ =>
   1.120 +      {
   1.121 +        case Text.Info(_, elem) =>
   1.122 +          if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
   1.123 +          else Some(Rendering.Color.quoted)
   1.124 +      })
   1.125 +
   1.126 +
   1.127    /* caret focus */
   1.128  
   1.129    private def entity_focus(range: Text.Range,
     2.1 --- a/src/Tools/jEdit/etc/options	Sat Mar 04 08:41:32 2017 +0100
     2.2 +++ b/src/Tools/jEdit/etc/options	Sat Mar 04 09:27:51 2017 +0100
     2.3 @@ -144,10 +144,10 @@
     2.4  option dynamic_color : string = "7BA428FF"
     2.5  option class_parameter_color : string = "D2691EFF"
     2.6  
     2.7 -option markdown_item_color1 : string = "DAFEDAFF"
     2.8 -option markdown_item_color2 : string = "FFF0CCFF"
     2.9 -option markdown_item_color3 : string = "E7E7FFFF"
    2.10 -option markdown_item_color4 : string = "FFE0F0FF"
    2.11 +option markdown_item1_color : string = "DAFEDAFF"
    2.12 +option markdown_item2_color : string = "FFF0CCFF"
    2.13 +option markdown_item3_color : string = "E7E7FFFF"
    2.14 +option markdown_item4_color : string = "FFE0F0FF"
    2.15  
    2.16  
    2.17  section "Icons"
     3.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Mar 04 08:41:32 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Mar 04 09:27:51 2017 +0100
     3.3 @@ -135,10 +135,6 @@
     3.4      Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,
     3.5        Markup.CITATION, Markup.URL)
     3.6  
     3.7 -  private val active_elements =
     3.8 -    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
     3.9 -      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
    3.10 -
    3.11    private val tooltip_message_elements =
    3.12      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    3.13        Markup.BAD)
    3.14 @@ -157,18 +153,6 @@
    3.15    private val separator_elements =
    3.16      Markup.Elements(Markup.SEPARATOR)
    3.17  
    3.18 -  private val background_elements =
    3.19 -    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    3.20 -      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    3.21 -      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    3.22 -      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    3.23 -      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    3.24 -      Markup.Markdown_Item.name ++ active_elements
    3.25 -
    3.26 -  private val foreground_elements =
    3.27 -    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    3.28 -      Markup.CARTOUCHE, Markup.ANTIQUOTED)
    3.29 -
    3.30    private val bullet_elements =
    3.31      Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
    3.32  
    3.33 @@ -184,11 +168,14 @@
    3.34  
    3.35    def color_value(s: String): Color = Color_Value(options.string(s))
    3.36  
    3.37 +  lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
    3.38 +    Rendering.Color.values.iterator.map(c => c -> color_value(c.toString + "_color")).toMap
    3.39 +
    3.40 +  def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
    3.41 +
    3.42    val outdated_color = color_value("outdated_color")
    3.43    val unprocessed_color = color_value("unprocessed_color")
    3.44 -  val unprocessed1_color = color_value("unprocessed1_color")
    3.45    val running_color = color_value("running_color")
    3.46 -  val running1_color = color_value("running1_color")
    3.47    val bullet_color = color_value("bullet_color")
    3.48    val tooltip_color = color_value("tooltip_color")
    3.49    val writeln_color = color_value("writeln_color")
    3.50 @@ -203,21 +190,14 @@
    3.51    val legacy_message_color = color_value("legacy_message_color")
    3.52    val error_message_color = color_value("error_message_color")
    3.53    val spell_checker_color = color_value("spell_checker_color")
    3.54 -  val bad_color = color_value("bad_color")
    3.55 -  val intensify_color = color_value("intensify_color")
    3.56 -  val entity_color = color_value("entity_color")
    3.57    val entity_ref_color = color_value("entity_ref_color")
    3.58    val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
    3.59    val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
    3.60    val caret_debugger_color = color_value("caret_debugger_color")
    3.61 -  val quoted_color = color_value("quoted_color")
    3.62 -  val antiquoted_color = color_value("antiquoted_color")
    3.63    val antiquote_color = color_value("antiquote_color")
    3.64    val highlight_color = color_value("highlight_color")
    3.65    val hyperlink_color = color_value("hyperlink_color")
    3.66 -  val active_color = color_value("active_color")
    3.67    val active_hover_color = color_value("active_hover_color")
    3.68 -  val active_result_color = color_value("active_result_color")
    3.69    val keyword1_color = color_value("keyword1_color")
    3.70    val keyword2_color = color_value("keyword2_color")
    3.71    val keyword3_color = color_value("keyword3_color")
    3.72 @@ -241,11 +221,6 @@
    3.73    val dynamic_color = color_value("dynamic_color")
    3.74    val class_parameter_color = color_value("class_parameter_color")
    3.75  
    3.76 -  val markdown_item_color1 = color_value("markdown_item_color1")
    3.77 -  val markdown_item_color2 = color_value("markdown_item_color2")
    3.78 -  val markdown_item_color3 = color_value("markdown_item_color3")
    3.79 -  val markdown_item_color4 = color_value("markdown_item_color4")
    3.80 -
    3.81  
    3.82    /* indentation */
    3.83  
    3.84 @@ -408,7 +383,7 @@
    3.85    /* active elements */
    3.86  
    3.87    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    3.88 -    snapshot.select(range, JEdit_Rendering.active_elements, command_states =>
    3.89 +    snapshot.select(range, Rendering.active_elements, command_states =>
    3.90        {
    3.91          case Text.Info(info_range, elem) =>
    3.92            if (elem.name == Markup.DIALOG) {
    3.93 @@ -562,74 +537,6 @@
    3.94    }
    3.95  
    3.96  
    3.97 -  /* text background */
    3.98 -
    3.99 -  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
   3.100 -  {
   3.101 -    for {
   3.102 -      Text.Info(r, result) <-
   3.103 -        snapshot.cumulate[(List[Markup], Option[Color])](
   3.104 -          range, (List(Markup.Empty), None), JEdit_Rendering.background_elements,
   3.105 -          command_states =>
   3.106 -            {
   3.107 -              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
   3.108 -              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
   3.109 -                Some((markup :: markups, color))
   3.110 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   3.111 -                Some((Nil, Some(bad_color)))
   3.112 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   3.113 -                Some((Nil, Some(intensify_color)))
   3.114 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
   3.115 -                props match {
   3.116 -                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(entity_color)))
   3.117 -                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(entity_color)))
   3.118 -                  case _ => None
   3.119 -                }
   3.120 -              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
   3.121 -                val color =
   3.122 -                  depth match {
   3.123 -                    case 1 => markdown_item_color1
   3.124 -                    case 2 => markdown_item_color2
   3.125 -                    case 3 => markdown_item_color3
   3.126 -                    case _ => markdown_item_color4
   3.127 -                  }
   3.128 -                Some((Nil, Some(color)))
   3.129 -              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
   3.130 -                command_states.collectFirst(
   3.131 -                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
   3.132 -                {
   3.133 -                  case Some(Protocol.Dialog_Result(res)) if res == result =>
   3.134 -                    Some((Nil, Some(active_result_color)))
   3.135 -                  case _ =>
   3.136 -                    Some((Nil, Some(active_color)))
   3.137 -                }
   3.138 -              case (_, Text.Info(_, elem)) =>
   3.139 -                if (JEdit_Rendering.active_elements(elem.name)) Some((Nil, Some(active_color)))
   3.140 -                else None
   3.141 -            })
   3.142 -      color <-
   3.143 -        (result match {
   3.144 -          case (markups, opt_color) if markups.nonEmpty =>
   3.145 -            val status = Protocol.Status.make(markups.iterator)
   3.146 -            if (status.is_unprocessed) Some(unprocessed1_color)
   3.147 -            else if (status.is_running) Some(running1_color)
   3.148 -            else opt_color
   3.149 -          case (_, opt_color) => opt_color
   3.150 -        })
   3.151 -    } yield Text.Info(r, color)
   3.152 -  }
   3.153 -
   3.154 -
   3.155 -  /* text foreground */
   3.156 -
   3.157 -  def foreground(range: Text.Range): List[Text.Info[Color]] =
   3.158 -    snapshot.select(range, JEdit_Rendering.foreground_elements, _ =>
   3.159 -      {
   3.160 -        case Text.Info(_, elem) =>
   3.161 -          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
   3.162 -      })
   3.163 -
   3.164 -
   3.165    /* text color */
   3.166  
   3.167    val foreground_color = jEdit.getColorProperty("view.fgColor")
     4.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 04 08:41:32 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Mar 04 09:27:51 2017 +0100
     4.3 @@ -309,10 +309,10 @@
     4.4  
     4.5              // background color
     4.6              for {
     4.7 -              Text.Info(range, color) <- rendering.background(line_range, caret_focus)
     4.8 +              Text.Info(range, c) <- rendering.background(line_range, caret_focus)
     4.9                r <- JEdit_Lib.gfx_range(text_area, range)
    4.10              } {
    4.11 -              gfx.setColor(color)
    4.12 +              gfx.setColor(rendering.color(c))
    4.13                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    4.14              }
    4.15  
    4.16 @@ -533,10 +533,10 @@
    4.17  
    4.18              // foreground color
    4.19              for {
    4.20 -              Text.Info(range, color) <- rendering.foreground(line_range)
    4.21 +              Text.Info(range, c) <- rendering.foreground(line_range)
    4.22                r <- JEdit_Lib.gfx_range(text_area, range)
    4.23              } {
    4.24 -              gfx.setColor(color)
    4.25 +              gfx.setColor(rendering.color(c))
    4.26                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    4.27              }
    4.28