| author | wenzelm |
| Fri, 10 Mar 2017 23:02:10 +0100 | |
| changeset 65178 | c4def7e9cfad |
| parent 65170 | 53675f36820d (current diff) |
| parent 65177 | 976938956460 (diff) |
| child 65179 | 883acfccb265 |
--- a/src/Pure/Isar/token.ML Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Pure/Isar/token.ML Fri Mar 10 23:02:10 2017 +0100 @@ -282,9 +282,11 @@ fun command_markups keywords x = if Keyword.is_theory_end keywords x then [Markup.keyword2] - else if Keyword.is_proof_asm keywords x then [Markup.keyword3] - else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] - else [Markup.keyword1]; + else + (if Keyword.is_proof_asm keywords x then [Markup.keyword3] + else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] + else [Markup.keyword1]) + |> map (Markup.properties [(Markup.kindN, Markup.commandN)]); in
--- a/src/Pure/PIDE/markup.scala Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Pure/PIDE/markup.scala Fri Mar 10 23:02:10 2017 +0100 @@ -29,6 +29,8 @@ def apply(elem: String): Boolean = rep.contains(elem) def + (elem: String): Elements = new Elements(rep + elem) def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep) + def - (elem: String): Elements = new Elements(rep - elem) + def -- (elems: Elements): Elements = new Elements(rep -- elems.rep) override def toString: String = rep.mkString("Elements(", ",", ")") }
--- a/src/Pure/PIDE/rendering.scala Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Fri Mar 10 23:02:10 2017 +0100 @@ -253,7 +253,8 @@ /* text background */ - def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] = + def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long]) + : List[Text.Info[Rendering.Color.Value]] = { for { Text.Info(r, result) <-
--- a/src/Tools/VSCode/extension/README.md Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/extension/README.md Fri Mar 10 23:02:10 2017 +0100 @@ -16,11 +16,6 @@ * On Windows: `isabelle.home` as above, but in Windows path notation with drive-letter and backslashes. - Moreover, `isabelle.cygwin_root` needs to point to a suitable Cygwin - installation, e.g. `$ISABELLE_HOME\contrib\cygwin` for a regular Isabelle - application bundle, or `C:\cygwin` for a stand-alone installation used - with Isabelle repository snapshot. - ## Isabelle symbols ##
--- a/src/Tools/VSCode/extension/package.json Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/extension/package.json Fri Mar 10 23:02:10 2017 +0100 @@ -52,11 +52,6 @@ "configuration": { "title": "Isabelle", "properties": { - "isabelle.cygwin_root": { - "type": "string", - "default": "", - "description": "Root of Cygwin installation on Windows (e.g. ISABELLE_HOME/cygwin)." - }, "isabelle.home": { "type": "string", "default": "", @@ -68,30 +63,29 @@ "default": [], "description": "Command-line arguments for isabelle vscode_server process." }, + "isabelle.cygwin_root": { + "type": "string", + "default": "", + "description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)." + }, "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.unprocessed1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.10)" }, + "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.40)" }, + "isabelle.running1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.20)" }, + "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, + "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" }, + "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.40)" }, + "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(204, 136, 0, 0.20)" }, "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_item1_dark_color": { "type": "string", "default": "rgba(5, 199, 5, 0.20)" }, "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_item2_dark_color": { "type": "string", "default": "rgba(204, 143, 0, 0.20)" }, "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_item3_dark_color": { "type": "string", "default": "rgba(0, 0, 204, 0.20)" }, "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.markdown_item4_dark_color": { "type": "string", "default": "rgba(204, 0, 105, 0.20)" }, "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.quoted_dark_color": { "type": "string", "default": "rgba(109, 109, 109, 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)" }, "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" }, @@ -101,45 +95,45 @@ "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }, - "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }, - "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" }, - "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" }, - "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" }, - "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" }, - "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" }, - "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" }, + "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" }, + "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(175, 0, 219, 1.00)" }, + "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }, + "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" }, + "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" }, + "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(38, 127, 153, 1.00)" }, + "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(78, 201, 176), 1.00)" }, "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, - "isabelle.improper_light_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" }, - "isabelle.improper_dark_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" }, + "isabelle.improper_light_color": { "type": "string", "default": "rgba(205, 49, 49, 1.00)" }, + "isabelle.improper_dark_color": { "type": "string", "default": "rgba(244, 71, 71, 1.00)" }, "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" }, - "isabelle.operator_dark_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" }, + "isabelle.operator_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" }, "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" }, - "isabelle.free_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" }, + "isabelle.free_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" }, "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.bound_dark_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, - "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" }, - "isabelle.var_dark_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" }, - "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" }, - "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" }, - "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" }, - "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" }, - "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" }, - "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" }, - "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" }, - "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" }, - "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" }, - "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" }, + "isabelle.bound_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, + "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 16, 128, 1.00)" }, + "isabelle.var_dark_color": { "type": "string", "default": "rgba(156, 220, 254, 1.00)" }, + "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" }, + "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" }, + "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(163, 21, 21, 1.00)" }, + "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(206, 145, 120, 1.00)" }, + "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(129, 31, 63, 1.00)" }, + "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(209, 105, 105, 1.00)" }, + "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, + "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" }, + "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(121, 94, 38, 1.00)" }, + "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(220, 220, 170, 1.00)" }, "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }, - "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" } + "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" } } } },
--- a/src/Tools/VSCode/extension/src/decorations.ts Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Fri Mar 10 23:02:10 2017 +0100 @@ -1,7 +1,7 @@ 'use strict'; import * as vscode from 'vscode' -import { Range, MarkedString, DecorationOptions, DecorationRenderOptions, +import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions, TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode' @@ -14,11 +14,8 @@ "running1", "bad", "intensify", - "entity", "quoted", "antiquoted", - "active", - "active_result", "markdown_item1", "markdown_item2", "markdown_item3", @@ -114,11 +111,16 @@ /* decoration for document node */ +interface DecorationOpts { + range: number[], + hover_message?: MarkedString | MarkedString[] +} + export interface Decoration { uri: string, "type": string, - content: DecorationOptions[] + content: DecorationOpts[] } type Content = Range[] | DecorationOptions[] @@ -129,24 +131,27 @@ document_decorations.delete(document.uri.toString()) } -export function apply_decoration(decoration0: Decoration) +export function apply_decoration(decoration: Decoration) { - const typ = types[decoration0.type] + const typ = types[decoration.type] if (typ) { - const decoration = - { - uri: Uri.parse(decoration0.uri).toString(), - "type": decoration0.type, - content: decoration0.content - } + const uri = Uri.parse(decoration.uri).toString() + const content: DecorationOptions[] = decoration.content.map(opt => + { + const r = opt.range + return { + range: new Range(new Position(r[0], r[1]), new Position(r[2], r[3])), + hoverMessage: opt.hover_message + } + }) - const document = document_decorations.get(decoration.uri) || new Map<string, Content>() - document.set(decoration.type, decoration.content) - document_decorations.set(decoration.uri, document) + const document = document_decorations.get(uri) || new Map<string, Content>() + document.set(decoration.type, content) + document_decorations.set(uri, document) for (const editor of vscode.window.visibleTextEditors) { - if (decoration.uri == editor.document.uri.toString()) { - editor.setDecorations(typ, decoration.content) + if (uri === editor.document.uri.toString()) { + editor.setDecorations(typ, content) } } }
--- a/src/Tools/VSCode/extension/src/extension.ts Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Fri Mar 10 23:02:10 2017 +0100 @@ -2,6 +2,7 @@ import * as vscode from 'vscode'; import * as path from 'path'; +import * as fs from 'fs'; import * as os from 'os'; import * as decorations from './decorations'; import { Decoration } from './decorations' @@ -13,13 +14,11 @@ { const is_windows = os.type().startsWith("Windows") - const cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root"); - const isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home"); - const isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args"); + const isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home") + const isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args") + const cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root") - if (is_windows && cygwin_root == "") - vscode.window.showErrorMessage("Missing user settings: isabelle.cygwin_root") - else if (isabelle_home == "") + if (isabelle_home === "") vscode.window.showErrorMessage("Missing user settings: isabelle.home") else { const isabelle_tool = isabelle_home + "/bin/isabelle" @@ -27,7 +26,9 @@ const server_options: ServerOptions = is_windows ? - { command: cygwin_root + "/bin/bash", + { command: + (cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) + + "/bin/bash", args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } : { command: isabelle_tool, args: ["vscode_server"].concat(standard_args, isabelle_args) };
--- a/src/Tools/VSCode/src/grammar.scala Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/src/grammar.scala Fri Mar 10 23:02:10 2017 +0100 @@ -82,7 +82,7 @@ "match": """ + grouped_names(keywords1) + """ }, { - "name": "keyword.other.isabelle", + "name": "keyword.other.unit.isabelle", "match": """ + grouped_names(keywords2) + """ }, { @@ -90,7 +90,7 @@ "match": """ + grouped_names(operators) + """ }, { - "name": "entity.name.function.isabelle", + "name": "entity.name.type.isabelle", "match": """ + grouped_names(keywords3) + """ }, {
--- a/src/Tools/VSCode/src/protocol.scala Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Fri Mar 10 23:02:10 2017 +0100 @@ -169,6 +169,9 @@ object Range { + def compact(range: Line.Range): List[Int] = + List(range.start.line, range.start.column, range.stop.line, range.stop.column) + def apply(range: Line.Range): JSON.T = Map("start" -> Position(range.start), "end" -> Position(range.stop)) @@ -404,21 +407,17 @@ /* decorations */ - sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString]) + sealed case class DecorationOpts(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" -> json_range) ++ - JSON.optional("hoverMessage" -> MarkedStrings.json(hover_message)) + Map("range" -> Range.compact(range)) ++ + JSON.optional("hover_message" -> MarkedStrings.json(hover_message)) } - sealed case class Decoration(typ: String, content: List[DecorationOptions]) + sealed case class Decoration(typ: String, content: List[DecorationOpts]) { - 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" -> json_content)) + Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) } }
--- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Mar 10 23:02:10 2017 +0100 @@ -28,6 +28,10 @@ Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) } + private val background_colors = + Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result - + Rendering.Color.entity + private val dotted_colors = Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning) @@ -45,6 +49,9 @@ private val diagnostics_elements = Markup.Elements(Markup.LEGACY, Markup.ERROR) + private val background_elements = + Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements + private val dotted_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING) @@ -117,7 +124,9 @@ { snapshot.select(range, Rendering.text_color_elements, _ => { - case Text.Info(_, elem) => Rendering.text_color.get(elem.name) + case Text.Info(_, XML.Elem(Markup(name, props), _)) => + if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None + else Rendering.text_color.get(name) }) } @@ -146,8 +155,8 @@ /* decorations */ def decorations: List[Document_Model.Decoration] = // list of canonical length and order - VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors, - background(model.content.text_range, Set.empty)) ::: + VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors, + background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) ::: VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, foreground(model.content.text_range)) ::: VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, @@ -162,7 +171,7 @@ for (Text.Info(text_range, msgs) <- decoration.content) yield { val range = model.content.doc.range(text_range) - Protocol.DecorationOptions(range, + Protocol.DecorationOpts(range, msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg)))) } Protocol.Decoration(decoration.typ, content)
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Mar 10 13:47:35 2017 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Mar 10 23:02:10 2017 +0100 @@ -309,7 +309,8 @@ // background color for { - Text.Info(range, c) <- rendering.background(line_range, caret_focus) + Text.Info(range, c) <- + rendering.background(Rendering.background_elements, line_range, caret_focus) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(rendering.color(c))