--- a/src/Pure/PIDE/rendering.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Mar 04 22:07:31 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,
--- a/src/Tools/VSCode/etc/options Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/etc/options Sat Mar 04 22:07:31 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
--- a/src/Tools/VSCode/extension/package.json Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json Sat Mar 04 22:07:31 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)" }
}
}
},
--- a/src/Tools/VSCode/extension/src/decorations.ts Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 04 22:07:31 2017 +0100
@@ -7,13 +7,36 @@
/* known decoration types */
-export interface Decorations
+export const types = new Map<string, TextEditorDecorationType>()
+
+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<string>(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({})
}
--- a/src/Tools/VSCode/src/document_model.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Sat Mar 04 22:07:31 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 */
--- a/src/Tools/VSCode/src/protocol.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala Sat Mar 04 22:07:31 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))
}
}
--- a/src/Tools/VSCode/src/server.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Sat Mar 04 22:07:31 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))
--- a/src/Tools/VSCode/src/vscode_rendering.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 22:07:31 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")
--- a/src/Tools/VSCode/src/vscode_resources.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Mar 04 22:07:31 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)
}
--- a/src/Tools/jEdit/etc/options Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/jEdit/etc/options Sat Mar 04 22:07:31 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 Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 04 22:07:31 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")
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Mar 02 21:16:02 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 04 22:07:31 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)
}