--- 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,
--- 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"
--- 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")
--- 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)
}