merged
authorwenzelm
Fri Mar 10 23:02:10 2017 +0100 (2017-03-10)
changeset 65178c4def7e9cfad
parent 65170 53675f36820d
parent 65177 976938956460
child 65179 883acfccb265
merged
     1.1 --- a/src/Pure/Isar/token.ML	Fri Mar 10 13:47:35 2017 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Fri Mar 10 23:02:10 2017 +0100
     1.3 @@ -282,9 +282,11 @@
     1.4  
     1.5  fun command_markups keywords x =
     1.6    if Keyword.is_theory_end keywords x then [Markup.keyword2]
     1.7 -  else if Keyword.is_proof_asm keywords x then [Markup.keyword3]
     1.8 -  else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
     1.9 -  else [Markup.keyword1];
    1.10 +  else
    1.11 +    (if Keyword.is_proof_asm keywords x then [Markup.keyword3]
    1.12 +     else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
    1.13 +     else [Markup.keyword1])
    1.14 +    |> map (Markup.properties [(Markup.kindN, Markup.commandN)]);
    1.15  
    1.16  in
    1.17  
     2.1 --- a/src/Pure/PIDE/markup.scala	Fri Mar 10 13:47:35 2017 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Fri Mar 10 23:02:10 2017 +0100
     2.3 @@ -29,6 +29,8 @@
     2.4      def apply(elem: String): Boolean = rep.contains(elem)
     2.5      def + (elem: String): Elements = new Elements(rep + elem)
     2.6      def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     2.7 +    def - (elem: String): Elements = new Elements(rep - elem)
     2.8 +    def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     2.9      override def toString: String = rep.mkString("Elements(", ",", ")")
    2.10    }
    2.11  
     3.1 --- a/src/Pure/PIDE/rendering.scala	Fri Mar 10 13:47:35 2017 +0100
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Fri Mar 10 23:02:10 2017 +0100
     3.3 @@ -253,7 +253,8 @@
     3.4  
     3.5    /* text background */
     3.6  
     3.7 -  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
     3.8 +  def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
     3.9 +    : List[Text.Info[Rendering.Color.Value]] =
    3.10    {
    3.11      for {
    3.12        Text.Info(r, result) <-
     4.1 --- a/src/Tools/VSCode/extension/README.md	Fri Mar 10 13:47:35 2017 +0100
     4.2 +++ b/src/Tools/VSCode/extension/README.md	Fri Mar 10 23:02:10 2017 +0100
     4.3 @@ -16,11 +16,6 @@
     4.4    * On Windows: `isabelle.home` as above, but in Windows path notation with
     4.5      drive-letter and backslashes.
     4.6  
     4.7 -    Moreover, `isabelle.cygwin_root` needs to point to a suitable Cygwin
     4.8 -    installation, e.g. `$ISABELLE_HOME\contrib\cygwin` for a regular Isabelle
     4.9 -    application bundle, or `C:\cygwin` for a stand-alone installation used
    4.10 -    with Isabelle repository snapshot.
    4.11 -
    4.12  
    4.13  ## Isabelle symbols ##
    4.14  
     5.1 --- a/src/Tools/VSCode/extension/package.json	Fri Mar 10 13:47:35 2017 +0100
     5.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Mar 10 23:02:10 2017 +0100
     5.3 @@ -52,11 +52,6 @@
     5.4          "configuration": {
     5.5              "title": "Isabelle",
     5.6              "properties": {
     5.7 -                "isabelle.cygwin_root": {
     5.8 -                    "type": "string",
     5.9 -                    "default": "",
    5.10 -                    "description": "Root of Cygwin installation on Windows (e.g. ISABELLE_HOME/cygwin)."
    5.11 -                },
    5.12                  "isabelle.home": {
    5.13                      "type": "string",
    5.14                      "default": "",
    5.15 @@ -68,30 +63,29 @@
    5.16                      "default": [],
    5.17                      "description": "Command-line arguments for isabelle vscode_server process."
    5.18                  },
    5.19 +                "isabelle.cygwin_root": {
    5.20 +                    "type": "string",
    5.21 +                    "default": "",
    5.22 +                    "description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)."
    5.23 +                },
    5.24                  "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" },
    5.25 -                "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" },
    5.26 -                "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" },
    5.27 -                "isabelle.running1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" },
    5.28 -                "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" },
    5.29 -                "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" },
    5.30 -                "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
    5.31 -                "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
    5.32 -                "isabelle.entity_light_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
    5.33 -                "isabelle.entity_dark_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
    5.34 -                "isabelle.active_light_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
    5.35 -                "isabelle.active_dark_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
    5.36 -                "isabelle.active_result_light_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
    5.37 -                "isabelle.active_result_dark_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
    5.38 +                "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.10)" },
    5.39 +                "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.40)" },
    5.40 +                "isabelle.running1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.20)" },
    5.41 +                "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" },
    5.42 +                "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" },
    5.43 +                "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.40)" },
    5.44 +                "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(204, 136, 0, 0.20)" },
    5.45                  "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
    5.46 -                "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
    5.47 +                "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(5, 199, 5, 0.20)" },
    5.48                  "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
    5.49 -                "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
    5.50 +                "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(204, 143, 0, 0.20)" },
    5.51                  "isabelle.markdown_item3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" },
    5.52 -                "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" },
    5.53 +                "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(0, 0, 204, 0.20)" },
    5.54                  "isabelle.markdown_item4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" },
    5.55 -                "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" },
    5.56 +                "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(204, 0, 105, 0.20)" },
    5.57                  "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
    5.58 -                "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
    5.59 +                "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(109, 109, 109, 0.10)" },
    5.60                  "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
    5.61                  "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
    5.62                  "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
    5.63 @@ -101,45 +95,45 @@
    5.64                  "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
    5.65                  "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
    5.66                  "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
    5.67 -                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
    5.68 -                "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" },
    5.69 -                "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" },
    5.70 -                "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" },
    5.71 -                "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" },
    5.72 -                "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" },
    5.73 -                "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" },
    5.74 +                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" },
    5.75 +                "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(175, 0, 219, 1.00)" },
    5.76 +                "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" },
    5.77 +                "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" },
    5.78 +                "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" },
    5.79 +                "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(38, 127, 153, 1.00)" },
    5.80 +                "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(78, 201, 176), 1.00)" },
    5.81                  "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
    5.82                  "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
    5.83 -                "isabelle.improper_light_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" },
    5.84 -                "isabelle.improper_dark_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" },
    5.85 +                "isabelle.improper_light_color": { "type": "string", "default": "rgba(205, 49, 49, 1.00)" },
    5.86 +                "isabelle.improper_dark_color": { "type": "string", "default": "rgba(244, 71, 71, 1.00)" },
    5.87                  "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
    5.88 -                "isabelle.operator_dark_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
    5.89 +                "isabelle.operator_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" },
    5.90                  "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    5.91                  "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    5.92                  "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    5.93                  "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    5.94                  "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
    5.95 -                "isabelle.free_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
    5.96 +                "isabelle.free_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" },
    5.97                  "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
    5.98                  "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
    5.99                  "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
   5.100 -                "isabelle.bound_dark_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
   5.101 -                "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" },
   5.102 -                "isabelle.var_dark_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" },
   5.103 -                "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" },
   5.104 -                "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" },
   5.105 -                "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" },
   5.106 -                "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" },
   5.107 -                "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" },
   5.108 -                "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" },
   5.109 -                "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" },
   5.110 -                "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" },
   5.111 -                "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" },
   5.112 -                "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" },
   5.113 +                "isabelle.bound_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" },
   5.114 +                "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 16, 128, 1.00)" },
   5.115 +                "isabelle.var_dark_color": { "type": "string", "default": "rgba(156, 220, 254, 1.00)" },
   5.116 +                "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" },
   5.117 +                "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" },
   5.118 +                "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(163, 21, 21, 1.00)" },
   5.119 +                "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(206, 145, 120, 1.00)" },
   5.120 +                "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(129, 31, 63, 1.00)" },
   5.121 +                "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(209, 105, 105, 1.00)" },
   5.122 +                "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
   5.123 +                "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" },
   5.124 +                "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(121, 94, 38, 1.00)" },
   5.125 +                "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(220, 220, 170, 1.00)" },
   5.126                  "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
   5.127                  "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
   5.128                  "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
   5.129 -                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }
   5.130 +                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }
   5.131              }
   5.132          }
   5.133      },
     6.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 13:47:35 2017 +0100
     6.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 23:02:10 2017 +0100
     6.3 @@ -1,7 +1,7 @@
     6.4  'use strict';
     6.5  
     6.6  import * as vscode from 'vscode'
     6.7 -import { Range, MarkedString, DecorationOptions, DecorationRenderOptions,
     6.8 +import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
     6.9    TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
    6.10  
    6.11  
    6.12 @@ -14,11 +14,8 @@
    6.13    "running1",
    6.14    "bad",
    6.15    "intensify",
    6.16 -  "entity",
    6.17    "quoted",
    6.18    "antiquoted",
    6.19 -  "active",
    6.20 -  "active_result",
    6.21    "markdown_item1",
    6.22    "markdown_item2",
    6.23    "markdown_item3",
    6.24 @@ -114,11 +111,16 @@
    6.25  
    6.26  /* decoration for document node */
    6.27  
    6.28 +interface DecorationOpts {
    6.29 +  range: number[],
    6.30 +  hover_message?: MarkedString | MarkedString[]
    6.31 +}
    6.32 +
    6.33  export interface Decoration
    6.34  {
    6.35    uri: string,
    6.36    "type": string,
    6.37 -  content: DecorationOptions[]
    6.38 +  content: DecorationOpts[]
    6.39  }
    6.40  
    6.41  type Content = Range[] | DecorationOptions[]
    6.42 @@ -129,24 +131,27 @@
    6.43    document_decorations.delete(document.uri.toString())
    6.44  }
    6.45  
    6.46 -export function apply_decoration(decoration0: Decoration)
    6.47 +export function apply_decoration(decoration: Decoration)
    6.48  {
    6.49 -  const typ = types[decoration0.type]
    6.50 +  const typ = types[decoration.type]
    6.51    if (typ) {
    6.52 -    const decoration =
    6.53 -    {
    6.54 -      uri: Uri.parse(decoration0.uri).toString(),
    6.55 -      "type": decoration0.type,
    6.56 -      content: decoration0.content
    6.57 -    }
    6.58 +    const uri = Uri.parse(decoration.uri).toString()
    6.59 +    const content: DecorationOptions[] = decoration.content.map(opt =>
    6.60 +      {
    6.61 +        const r = opt.range
    6.62 +        return {
    6.63 +          range: new Range(new Position(r[0], r[1]), new Position(r[2], r[3])),
    6.64 +          hoverMessage: opt.hover_message
    6.65 +        }
    6.66 +      })
    6.67  
    6.68 -    const document = document_decorations.get(decoration.uri) || new Map<string, Content>()
    6.69 -    document.set(decoration.type, decoration.content)
    6.70 -    document_decorations.set(decoration.uri, document)
    6.71 +    const document = document_decorations.get(uri) || new Map<string, Content>()
    6.72 +    document.set(decoration.type, content)
    6.73 +    document_decorations.set(uri, document)
    6.74  
    6.75      for (const editor of vscode.window.visibleTextEditors) {
    6.76 -      if (decoration.uri == editor.document.uri.toString()) {
    6.77 -        editor.setDecorations(typ, decoration.content)
    6.78 +      if (uri === editor.document.uri.toString()) {
    6.79 +        editor.setDecorations(typ, content)
    6.80        }
    6.81      }
    6.82    }
     7.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Fri Mar 10 13:47:35 2017 +0100
     7.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Mar 10 23:02:10 2017 +0100
     7.3 @@ -2,6 +2,7 @@
     7.4  
     7.5  import * as vscode from 'vscode';
     7.6  import * as path from 'path';
     7.7 +import * as fs from 'fs';
     7.8  import * as os from 'os';
     7.9  import * as decorations from './decorations';
    7.10  import { Decoration } from './decorations'
    7.11 @@ -13,13 +14,11 @@
    7.12  {
    7.13    const is_windows = os.type().startsWith("Windows")
    7.14  
    7.15 -  const cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root");
    7.16 -  const isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home");
    7.17 -  const isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args");
    7.18 +  const isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home")
    7.19 +  const isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args")
    7.20 +  const cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root")
    7.21  
    7.22 -  if (is_windows && cygwin_root == "")
    7.23 -    vscode.window.showErrorMessage("Missing user settings: isabelle.cygwin_root")
    7.24 -  else if (isabelle_home == "")
    7.25 +  if (isabelle_home === "")
    7.26      vscode.window.showErrorMessage("Missing user settings: isabelle.home")
    7.27    else {
    7.28      const isabelle_tool = isabelle_home + "/bin/isabelle"
    7.29 @@ -27,7 +26,9 @@
    7.30  
    7.31      const server_options: ServerOptions =
    7.32        is_windows ?
    7.33 -        { command: cygwin_root + "/bin/bash",
    7.34 +        { command:
    7.35 +            (cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) +
    7.36 +            "/bin/bash",
    7.37            args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
    7.38          { command: isabelle_tool,
    7.39            args: ["vscode_server"].concat(standard_args, isabelle_args) };
     8.1 --- a/src/Tools/VSCode/src/grammar.scala	Fri Mar 10 13:47:35 2017 +0100
     8.2 +++ b/src/Tools/VSCode/src/grammar.scala	Fri Mar 10 23:02:10 2017 +0100
     8.3 @@ -82,7 +82,7 @@
     8.4        "match": """ + grouped_names(keywords1) + """
     8.5      },
     8.6      {
     8.7 -      "name": "keyword.other.isabelle",
     8.8 +      "name": "keyword.other.unit.isabelle",
     8.9        "match": """ + grouped_names(keywords2) + """
    8.10      },
    8.11      {
    8.12 @@ -90,7 +90,7 @@
    8.13        "match": """ + grouped_names(operators) + """
    8.14      },
    8.15      {
    8.16 -      "name": "entity.name.function.isabelle",
    8.17 +      "name": "entity.name.type.isabelle",
    8.18        "match": """ + grouped_names(keywords3) + """
    8.19      },
    8.20      {
     9.1 --- a/src/Tools/VSCode/src/protocol.scala	Fri Mar 10 13:47:35 2017 +0100
     9.2 +++ b/src/Tools/VSCode/src/protocol.scala	Fri Mar 10 23:02:10 2017 +0100
     9.3 @@ -169,6 +169,9 @@
     9.4  
     9.5    object Range
     9.6    {
     9.7 +    def compact(range: Line.Range): List[Int] =
     9.8 +      List(range.start.line, range.start.column, range.stop.line, range.stop.column)
     9.9 +
    9.10      def apply(range: Line.Range): JSON.T =
    9.11        Map("start" -> Position(range.start), "end" -> Position(range.stop))
    9.12  
    9.13 @@ -404,21 +407,17 @@
    9.14  
    9.15    /* decorations */
    9.16  
    9.17 -  sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
    9.18 +  sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString])
    9.19    {
    9.20 -    def no_hover_message: Boolean = hover_message.isEmpty
    9.21 -    def json_range: JSON.T = Range(range)
    9.22      def json: JSON.T =
    9.23 -      Map("range" -> json_range) ++
    9.24 -      JSON.optional("hoverMessage" -> MarkedStrings.json(hover_message))
    9.25 +      Map("range" -> Range.compact(range)) ++
    9.26 +      JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
    9.27    }
    9.28  
    9.29 -  sealed case class Decoration(typ: String, content: List[DecorationOptions])
    9.30 +  sealed case class Decoration(typ: String, content: List[DecorationOpts])
    9.31    {
    9.32 -    def json_content: JSON.T =
    9.33 -      if (content.forall(_.no_hover_message)) content.map(_.json_range) else content.map(_.json)
    9.34      def json(file: JFile): JSON.T =
    9.35        Notification("PIDE/decoration",
    9.36 -        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> json_content))
    9.37 +        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
    9.38    }
    9.39  }
    10.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 13:47:35 2017 +0100
    10.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 23:02:10 2017 +0100
    10.3 @@ -28,6 +28,10 @@
    10.4        Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
    10.5    }
    10.6  
    10.7 +  private val background_colors =
    10.8 +    Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
    10.9 +      Rendering.Color.entity
   10.10 +
   10.11    private val dotted_colors =
   10.12      Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
   10.13  
   10.14 @@ -45,6 +49,9 @@
   10.15    private val diagnostics_elements =
   10.16      Markup.Elements(Markup.LEGACY, Markup.ERROR)
   10.17  
   10.18 +  private val background_elements =
   10.19 +    Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
   10.20 +
   10.21    private val dotted_elements =
   10.22      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
   10.23  
   10.24 @@ -117,7 +124,9 @@
   10.25    {
   10.26      snapshot.select(range, Rendering.text_color_elements, _ =>
   10.27        {
   10.28 -        case Text.Info(_, elem) => Rendering.text_color.get(elem.name)
   10.29 +        case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
   10.30 +          if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
   10.31 +          else Rendering.text_color.get(name)
   10.32        })
   10.33    }
   10.34  
   10.35 @@ -146,8 +155,8 @@
   10.36    /* decorations */
   10.37  
   10.38    def decorations: List[Document_Model.Decoration] = // list of canonical length and order
   10.39 -    VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors,
   10.40 -      background(model.content.text_range, Set.empty)) :::
   10.41 +    VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
   10.42 +      background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) :::
   10.43      VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
   10.44        foreground(model.content.text_range)) :::
   10.45      VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
   10.46 @@ -162,7 +171,7 @@
   10.47        for (Text.Info(text_range, msgs) <- decoration.content)
   10.48        yield {
   10.49          val range = model.content.doc.range(text_range)
   10.50 -        Protocol.DecorationOptions(range,
   10.51 +        Protocol.DecorationOpts(range,
   10.52            msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
   10.53        }
   10.54      Protocol.Decoration(decoration.typ, content)
    11.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 13:47:35 2017 +0100
    11.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 23:02:10 2017 +0100
    11.3 @@ -309,7 +309,8 @@
    11.4  
    11.5              // background color
    11.6              for {
    11.7 -              Text.Info(range, c) <- rendering.background(line_range, caret_focus)
    11.8 +              Text.Info(range, c) <-
    11.9 +                rendering.background(Rendering.background_elements, line_range, caret_focus)
   11.10                r <- JEdit_Lib.gfx_range(text_area, range)
   11.11              } {
   11.12                gfx.setColor(rendering.color(c))