# HG changeset patch # User nipkow # Date 1488712056 -3600 # Node ID 73cd69353f7f9e5a13f46aa278d5704a372b84c2 # Parent 5a290f1819e5191410f90acabe493e75ce484c86# Parent a79c1080f1e98cec789d9b9de4f4afc1d7d65877 merged diff -r a79c1080f1e9 -r 73cd69353f7f src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Sun Mar 05 12:07:36 2017 +0100 @@ -10,6 +10,31 @@ object Rendering { + /* color */ + + object Color extends Enumeration + { + // background + val unprocessed1 = Value("unprocessed1") + val running1 = Value("running1") + val bad = Value("bad") + val intensify = Value("intensify") + val entity = Value("entity") + 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") + val background = values + + // foreground + val quoted = Value("quoted") + val antiquoted = Value("antiquoted") + val foreground = values -- background + } + + /* message priorities */ val state_pri = 1 @@ -39,6 +64,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) @@ -93,7 +134,6 @@ /* tooltips */ - def tooltip_margin: Int def timing_threshold: Double def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] = @@ -187,6 +227,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 a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/etc/options --- a/src/Tools/VSCode/etc/options Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/etc/options Sun Mar 05 12:07:36 2017 +0100 @@ -12,7 +12,7 @@ option vscode_tooltip_margin : int = 60 -- "margin for pretty-printing of tooltips" -option vscode_diagnostics_margin : int = 80 +option vscode_message_margin : int = 80 -- "margin for pretty-printing of diagnostic messages" option vscode_timing_threshold : real = 0.1 diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/extension/package.json Sun Mar 05 12:07:36 2017 +0100 @@ -67,7 +67,33 @@ "items": { "type": "string" }, "default": [], "description": "Command-line arguments for isabelle vscode_server process." - } + }, + "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" }, + "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" }, + "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" }, + "isabelle.running1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" }, + "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" }, + "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" }, + "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" }, + "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" }, + "isabelle.entity_light_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" }, + "isabelle.entity_dark_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" }, + "isabelle.active_light_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" }, + "isabelle.active_dark_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" }, + "isabelle.active_result_light_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" }, + "isabelle.active_result_dark_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" }, + "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" }, + "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" }, + "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" }, + "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" }, + "isabelle.markdown_item3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" }, + "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" }, + "isabelle.markdown_item4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" }, + "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" }, + "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" }, + "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" }, + "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" }, + "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" } } } }, diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 05 12:07:36 2017 +0100 @@ -7,13 +7,36 @@ /* known decoration types */ -export interface Decorations +export const types = new Map() + +const background_colors = [ + "unprocessed1", + "running1", + "bad", + "intensify", + "entity", + "quoted", + "antiquoted", + "active", + "active_result", + "markdown_item1", + "markdown_item2", + "markdown_item3", + "markdown_item4" +] + +const foreground_colors = [ + "quoted", + "antiquoted" +] + +function property(prop: string, config: string): Object { - bad: TextEditorDecorationType + let res = {} + res[prop] = vscode.workspace.getConfiguration("isabelle").get(config) + return res } -export let types: Decorations - export function init(context: ExtensionContext) { function decoration(options: DecorationRenderOptions): TextEditorDecorationType @@ -23,11 +46,22 @@ return typ } - if (!types) - types = - { - bad: decoration({ backgroundColor: 'rgba(255, 106, 106, 0.4)' }) - } + function background(color: string): TextEditorDecorationType + { + const prop = "backgroundColor" + const light = property(prop, color.concat("_light_color")) + const dark = property(prop, color.concat("_dark_color")) + return decoration({ light: light, dark: dark }) + } + + types.clear + for (let color of background_colors) { + types["background_".concat(color)] = background(color) + } + for (let color of foreground_colors) { + types["foreground_".concat(color)] = background(color) // approximation + } + types["hover_message"] = decoration({}) } diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sun Mar 05 12:07:36 2017 +0100 @@ -16,7 +16,7 @@ { /* decorations */ - sealed case class Decoration(typ: String, content: List[Text.Info[XML.Body]]) + sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) /* content */ diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Sun Mar 05 12:07:36 2017 +0100 @@ -205,13 +205,23 @@ } - /* marked string */ + /* marked strings */ sealed case class MarkedString(text: String, language: String = "plaintext") { def json: JSON.T = Map("language" -> language, "value" -> text) } + object MarkedStrings + { + def json(msgs: List[MarkedString]): Option[JSON.T] = + msgs match { + case Nil => None + case List(msg) => Some(msg.json) + case _ => Some(msgs.map(_.json)) + } + } + /* diagnostic messages */ @@ -335,7 +345,7 @@ val res = result match { case Some((range, contents)) => - Map("contents" -> contents.map(_.json), "range" -> Range(range)) + Map("contents" -> MarkedStrings.json(contents).getOrElse(Nil), "range" -> Range(range)) case None => Map("contents" -> Nil) } ResponseMessage(id, Some(res)) @@ -407,23 +417,21 @@ /* decorations */ - object Decorations - { - val bad = "bad" - } - sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString]) { + def no_hover_message: Boolean = hover_message.isEmpty + def json_range: JSON.T = Range(range) def json: JSON.T = - Map("range" -> Range(range)) ++ - JSON.optional("hoverMessage" -> - (if (hover_message.isEmpty) None else Some(hover_message.map(_.json)))) + Map("range" -> json_range) ++ + JSON.optional("hoverMessage" -> MarkedStrings.json(hover_message)) } sealed case class Decoration(typ: String, content: List[DecorationOptions]) { + def json_content: JSON.T = + if (content.forall(_.no_hover_message)) content.map(_.json_range) else content.map(_.json) def json(file: JFile): JSON.T = Notification("PIDE/decoration", - Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) + Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> json_content)) } } diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sun Mar 05 12:07:36 2017 +0100 @@ -300,8 +300,7 @@ val doc = rendering.model.content.doc val range = doc.range(info.range) val contents = - info.info.map(tree => - Protocol.MarkedString(resources.output_pretty(List(tree), rendering.tooltip_margin))) + info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) (range, contents) } channel.write(Protocol.Hover.reply(id, result)) diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Mar 05 12:07:36 2017 +0100 @@ -15,6 +15,21 @@ object VSCode_Rendering { + /* decorations */ + + private def color_decorations(prefix: String, types: Rendering.Color.ValueSet, + colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] = + { + val color_ranges = + (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) { + case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) + } + types.toList.map(c => + Document_Model.Decoration(prefix + c.toString, + color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: List[XML.Body])))) + } + + /* diagnostic messages */ private val message_severity = @@ -31,7 +46,7 @@ private val diagnostics_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) - private val bad_elements = Markup.Elements(Markup.BAD) + private val hover_message_elements = Markup.Elements(Markup.BAD) private val hyperlink_elements = Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION) @@ -78,8 +93,6 @@ case _ => None }).filterNot(info => info.info.is_empty) - val diagnostics_margin = options.int("vscode_diagnostics_margin") - def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] = { (for { @@ -87,7 +100,7 @@ range = model.content.doc.range(text_range) (_, XML.Elem(Markup(name, _), body)) <- res.iterator } yield { - val message = resources.output_pretty(body, diagnostics_margin) + val message = resources.output_pretty_message(body) val severity = VSCode_Rendering.message_severity.get(name) Protocol.Diagnostic(range, message, severity = severity) }).toList @@ -96,23 +109,40 @@ /* decorations */ - def decorations: List[Document_Model.Decoration] = - List(Document_Model.Decoration(Protocol.Decorations.bad, decorations_bad)) + def hover_message: Document_Model.Decoration = + { + val results = + snapshot.cumulate[Command.Results]( + model.content.text_range, Command.Results.empty, + VSCode_Rendering.hover_message_elements, _ => + { + case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) + if body.nonEmpty => + Some(msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))) - def decorations_bad: List[Text.Info[XML.Body]] = - snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ => - { - case Text.Info(_, XML.Elem(_, body)) => Some(body) - }) + case _ => None + }) + val content = + for (Text.Info(r, msgs) <- results if !msgs.is_empty) + yield Text.Info(r, (for ((_, t) <- msgs.iterator) yield List(t)).toList) + Document_Model.Decoration("hover_message", content) + } + + def decorations: List[Document_Model.Decoration] = + hover_message :: + VSCode_Rendering.color_decorations("background_", Rendering.Color.background, + background(model.content.text_range, Set.empty)) ::: + VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground, + foreground(model.content.text_range)) def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration = { val content = - for (Text.Info(text_range, body) <- decoration.content) + for (Text.Info(text_range, msgs) <- decoration.content) yield { val range = model.content.doc.range(text_range) - val msg = resources.output_pretty(body, diagnostics_margin) - Protocol.DecorationOptions(range, if (msg == "") Nil else List(Protocol.MarkedString(msg))) + Protocol.DecorationOptions(range, + msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg)))) } Protocol.Decoration(decoration.typ, content) } @@ -120,7 +150,6 @@ /* tooltips */ - def tooltip_margin: Int = options.int("vscode_tooltip_margin") def timing_threshold: Double = options.real("vscode_timing_threshold") diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Mar 05 12:07:36 2017 +0100 @@ -259,13 +259,17 @@ /* output text */ def decode_text: Boolean = options.bool("vscode_unicode_symbols") + def tooltip_margin: Int = options.int("vscode_tooltip_margin") + def message_margin: Int = options.int("vscode_message_margin") def output_text(s: String): String = if (decode_text) Symbol.decode(s) else Symbol.encode(s) + def output_xml(xml: XML.Tree): String = + output_text(XML.content(xml)) + def output_pretty(body: XML.Body, margin: Int): String = output_text(Pretty.string_of(body, margin)) - - def output_xml(xml: XML.Tree): String = - output_text(XML.content(xml)) + def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) + def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) } diff -r a79c1080f1e9 -r 73cd69353f7f src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/jEdit/etc/options Sun Mar 05 12:07:36 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 a79c1080f1e9 -r 73cd69353f7f src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Mar 05 12:07:36 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) @@ -182,69 +166,60 @@ { /* colors */ - def color_value(s: String): Color = Color_Value(options.string(s)) + def color(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(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") - val information_color = color_value("information_color") - val warning_color = color_value("warning_color") - val legacy_color = color_value("legacy_color") - val error_color = color_value("error_color") - val writeln_message_color = color_value("writeln_message_color") - val information_message_color = color_value("information_message_color") - val tracing_message_color = color_value("tracing_message_color") - val warning_message_color = color_value("warning_message_color") - 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") - val quasi_keyword_color = color_value("quasi_keyword_color") - val improper_color = color_value("improper_color") - val operator_color = color_value("operator_color") - val caret_invisible_color = color_value("caret_invisible_color") - val completion_color = color_value("completion_color") - val search_color = color_value("search_color") + val outdated_color = color("outdated_color") + val unprocessed_color = color("unprocessed_color") + val running_color = color("running_color") + val bullet_color = color("bullet_color") + val tooltip_color = color("tooltip_color") + val writeln_color = color("writeln_color") + val information_color = color("information_color") + val warning_color = color("warning_color") + val legacy_color = color("legacy_color") + val error_color = color("error_color") + val writeln_message_color = color("writeln_message_color") + val information_message_color = color("information_message_color") + val tracing_message_color = color("tracing_message_color") + val warning_message_color = color("warning_message_color") + val legacy_message_color = color("legacy_message_color") + val error_message_color = color("error_message_color") + val spell_checker_color = color("spell_checker_color") + val entity_ref_color = color("entity_ref_color") + val breakpoint_disabled_color = color("breakpoint_disabled_color") + val breakpoint_enabled_color = color("breakpoint_enabled_color") + val caret_debugger_color = color("caret_debugger_color") + val antiquote_color = color("antiquote_color") + val highlight_color = color("highlight_color") + val hyperlink_color = color("hyperlink_color") + val active_hover_color = color("active_hover_color") + val keyword1_color = color("keyword1_color") + val keyword2_color = color("keyword2_color") + val keyword3_color = color("keyword3_color") + val quasi_keyword_color = color("quasi_keyword_color") + val improper_color = color("improper_color") + val operator_color = color("operator_color") + val caret_invisible_color = color("caret_invisible_color") + val completion_color = color("completion_color") + val search_color = color("search_color") - val tfree_color = color_value("tfree_color") - val tvar_color = color_value("tvar_color") - val free_color = color_value("free_color") - val skolem_color = color_value("skolem_color") - val bound_color = color_value("bound_color") - val var_color = color_value("var_color") - val inner_numeral_color = color_value("inner_numeral_color") - val inner_quoted_color = color_value("inner_quoted_color") - val inner_cartouche_color = color_value("inner_cartouche_color") - val inner_comment_color = color_value("inner_comment_color") - 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") + val tfree_color = color("tfree_color") + val tvar_color = color("tvar_color") + val free_color = color("free_color") + val skolem_color = color("skolem_color") + val bound_color = color("bound_color") + val var_color = color("var_color") + val inner_numeral_color = color("inner_numeral_color") + val inner_quoted_color = color("inner_quoted_color") + val inner_cartouche_color = color("inner_cartouche_color") + val inner_comment_color = color("inner_comment_color") + val dynamic_color = color("dynamic_color") + val class_parameter_color = color("class_parameter_color") /* 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 (((status, color), Text.Info(_, XML.Elem(markup, _)))) - if status.nonEmpty && Protocol.proper_status_elements(markup.name) => - Some((markup :: status, 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 a79c1080f1e9 -r 73cd69353f7f src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Sun Mar 05 10:57:51 2017 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Mar 05 12:07:36 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) }