# HG changeset patch # User wenzelm # Date 1488616071 -3600 # Node ID 4263b2a201b3165e98186a1a4384124875b8fe71 # Parent 83d1f210a1d3caad915bddc83dcdb7126d7ba75b symbolic Rendering.Color; clarified modules; diff -r 83d1f210a1d3 -r 4263b2a201b3 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Mar 04 08:41:32 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Sat Mar 04 09:27:51 2017 +0100 @@ -10,6 +10,26 @@ object Rendering { + /* color */ + + object Color extends Enumeration + { + val unprocessed1 = Value("unprocessed1") + val running1 = Value("running1") + val bad = Value("bad") + val intensify = Value("intensify") + val entity = Value("entity") + val quoted = Value("quoted") + val antiquoted = Value("antiquoted") + val active = Value("active") + val active_result = Value("active_result") + val markdown_item1 = Value("markdown_item1") + val markdown_item2 = Value("markdown_item2") + val markdown_item3 = Value("markdown_item3") + val markdown_item4 = Value("markdown_item4") + } + + /* message priorities */ val state_pri = 1 @@ -39,6 +59,22 @@ /* markup elements */ + val active_elements = + Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, + Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) + + private val background_elements = + Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + + Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + + Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + + Markup.Markdown_Item.name ++ active_elements + + private val foreground_elements = + Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, + Markup.CARTOUCHE, Markup.ANTIQUOTED) + private val semantic_completion_elements = Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) @@ -187,6 +223,76 @@ } + /* text background */ + + def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] = + { + for { + Text.Info(r, result) <- + snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])]( + range, (List(Markup.Empty), None), Rendering.background_elements, + command_states => + { + case (((markups, color), Text.Info(_, XML.Elem(markup, _)))) + if markups.nonEmpty && Protocol.proper_status_elements(markup.name) => + Some((markup :: markups, color)) + case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => + Some((Nil, Some(Rendering.Color.bad))) + case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => + Some((Nil, Some(Rendering.Color.intensify))) + case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) + case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity))) + case _ => None + } + case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) => + val color = + depth match { + case 1 => Rendering.Color.markdown_item1 + case 2 => Rendering.Color.markdown_item2 + case 3 => Rendering.Color.markdown_item3 + case _ => Rendering.Color.markdown_item4 + } + Some((Nil, Some(color))) + case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => + command_states.collectFirst( + { case st if st.results.defined(serial) => st.results.get(serial).get }) match + { + case Some(Protocol.Dialog_Result(res)) if res == result => + Some((Nil, Some(Rendering.Color.active_result))) + case _ => + Some((Nil, Some(Rendering.Color.active))) + } + case (_, Text.Info(_, elem)) => + if (Rendering.active_elements(elem.name)) + Some((Nil, Some(Rendering.Color.active))) + else None + }) + color <- + (result match { + case (markups, opt_color) if markups.nonEmpty => + val status = Protocol.Status.make(markups.iterator) + if (status.is_unprocessed) Some(Rendering.Color.unprocessed1) + else if (status.is_running) Some(Rendering.Color.running1) + else opt_color + case (_, opt_color) => opt_color + }) + } yield Text.Info(r, color) + } + + + /* text foreground */ + + def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = + snapshot.select(range, Rendering.foreground_elements, _ => + { + case Text.Info(_, elem) => + if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted) + else Some(Rendering.Color.quoted) + }) + + /* caret focus */ private def entity_focus(range: Text.Range, diff -r 83d1f210a1d3 -r 4263b2a201b3 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Mar 04 08:41:32 2017 +0100 +++ b/src/Tools/jEdit/etc/options Sat Mar 04 09:27:51 2017 +0100 @@ -144,10 +144,10 @@ option dynamic_color : string = "7BA428FF" option class_parameter_color : string = "D2691EFF" -option markdown_item_color1 : string = "DAFEDAFF" -option markdown_item_color2 : string = "FFF0CCFF" -option markdown_item_color3 : string = "E7E7FFFF" -option markdown_item_color4 : string = "FFE0F0FF" +option markdown_item1_color : string = "DAFEDAFF" +option markdown_item2_color : string = "FFF0CCFF" +option markdown_item3_color : string = "E7E7FFFF" +option markdown_item4_color : string = "FFE0F0FF" section "Icons" diff -r 83d1f210a1d3 -r 4263b2a201b3 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 04 08:41:32 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 04 09:27:51 2017 +0100 @@ -135,10 +135,6 @@ Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION, Markup.CITATION, Markup.URL) - private val active_elements = - Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, - Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) - private val tooltip_message_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, Markup.BAD) @@ -157,18 +153,6 @@ private val separator_elements = Markup.Elements(Markup.SEPARATOR) - private val background_elements = - Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + - Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + - Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + - Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + - Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + - Markup.Markdown_Item.name ++ active_elements - - private val foreground_elements = - Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, - Markup.CARTOUCHE, Markup.ANTIQUOTED) - private val bullet_elements = Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT) @@ -184,11 +168,14 @@ def color_value(s: String): Color = Color_Value(options.string(s)) + lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = + Rendering.Color.values.iterator.map(c => c -> color_value(c.toString + "_color")).toMap + + def color(c: Rendering.Color.Value): Color = _rendering_colors(c) + val outdated_color = color_value("outdated_color") val unprocessed_color = color_value("unprocessed_color") - val unprocessed1_color = color_value("unprocessed1_color") val running_color = color_value("running_color") - val running1_color = color_value("running1_color") val bullet_color = color_value("bullet_color") val tooltip_color = color_value("tooltip_color") val writeln_color = color_value("writeln_color") @@ -203,21 +190,14 @@ val legacy_message_color = color_value("legacy_message_color") val error_message_color = color_value("error_message_color") val spell_checker_color = color_value("spell_checker_color") - val bad_color = color_value("bad_color") - val intensify_color = color_value("intensify_color") - val entity_color = color_value("entity_color") val entity_ref_color = color_value("entity_ref_color") val breakpoint_disabled_color = color_value("breakpoint_disabled_color") val breakpoint_enabled_color = color_value("breakpoint_enabled_color") val caret_debugger_color = color_value("caret_debugger_color") - val quoted_color = color_value("quoted_color") - val antiquoted_color = color_value("antiquoted_color") val antiquote_color = color_value("antiquote_color") val highlight_color = color_value("highlight_color") val hyperlink_color = color_value("hyperlink_color") - val active_color = color_value("active_color") val active_hover_color = color_value("active_hover_color") - val active_result_color = color_value("active_result_color") val keyword1_color = color_value("keyword1_color") val keyword2_color = color_value("keyword2_color") val keyword3_color = color_value("keyword3_color") @@ -241,11 +221,6 @@ val dynamic_color = color_value("dynamic_color") val class_parameter_color = color_value("class_parameter_color") - val markdown_item_color1 = color_value("markdown_item_color1") - val markdown_item_color2 = color_value("markdown_item_color2") - val markdown_item_color3 = color_value("markdown_item_color3") - val markdown_item_color4 = color_value("markdown_item_color4") - /* indentation */ @@ -408,7 +383,7 @@ /* active elements */ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = - snapshot.select(range, JEdit_Rendering.active_elements, command_states => + snapshot.select(range, Rendering.active_elements, command_states => { case Text.Info(info_range, elem) => if (elem.name == Markup.DIALOG) { @@ -562,74 +537,6 @@ } - /* text background */ - - def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = - { - for { - Text.Info(r, result) <- - snapshot.cumulate[(List[Markup], Option[Color])]( - range, (List(Markup.Empty), None), JEdit_Rendering.background_elements, - command_states => - { - case (((markups, color), Text.Info(_, XML.Elem(markup, _)))) - if markups.nonEmpty && Protocol.proper_status_elements(markup.name) => - Some((markup :: markups, color)) - case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => - Some((Nil, Some(bad_color))) - case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => - Some((Nil, Some(intensify_color))) - case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => - props match { - case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(entity_color))) - case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(entity_color))) - case _ => None - } - case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) => - val color = - depth match { - case 1 => markdown_item_color1 - case 2 => markdown_item_color2 - case 3 => markdown_item_color3 - case _ => markdown_item_color4 - } - Some((Nil, Some(color))) - case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => - command_states.collectFirst( - { case st if st.results.defined(serial) => st.results.get(serial).get }) match - { - case Some(Protocol.Dialog_Result(res)) if res == result => - Some((Nil, Some(active_result_color))) - case _ => - Some((Nil, Some(active_color))) - } - case (_, Text.Info(_, elem)) => - if (JEdit_Rendering.active_elements(elem.name)) Some((Nil, Some(active_color))) - else None - }) - color <- - (result match { - case (markups, opt_color) if markups.nonEmpty => - val status = Protocol.Status.make(markups.iterator) - if (status.is_unprocessed) Some(unprocessed1_color) - else if (status.is_running) Some(running1_color) - else opt_color - case (_, opt_color) => opt_color - }) - } yield Text.Info(r, color) - } - - - /* text foreground */ - - def foreground(range: Text.Range): List[Text.Info[Color]] = - snapshot.select(range, JEdit_Rendering.foreground_elements, _ => - { - case Text.Info(_, elem) => - if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color) - }) - - /* text color */ val foreground_color = jEdit.getColorProperty("view.fgColor") diff -r 83d1f210a1d3 -r 4263b2a201b3 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 04 08:41:32 2017 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 04 09:27:51 2017 +0100 @@ -309,10 +309,10 @@ // background color for { - Text.Info(range, color) <- rendering.background(line_range, caret_focus) + Text.Info(range, c) <- rendering.background(line_range, caret_focus) r <- JEdit_Lib.gfx_range(text_area, range) } { - gfx.setColor(color) + gfx.setColor(rendering.color(c)) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } @@ -533,10 +533,10 @@ // foreground color for { - Text.Info(range, color) <- rendering.foreground(line_range) + Text.Info(range, c) <- rendering.foreground(line_range) r <- JEdit_Lib.gfx_range(text_area, range) } { - gfx.setColor(color) + gfx.setColor(rendering.color(c)) gfx.fillRect(r.x, y + i * line_height, r.length, line_height) }