src/Tools/VSCode/src/grammar.scala
changeset 64746 34db87033abe
parent 64745 0f002c15f3ab
child 64808 81a5473e6d04
     1.1 --- a/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 10:22:59 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 10:59:46 2017 +0100
     1.3 @@ -57,14 +57,8 @@
     1.4          {
     1.5            "name": "comment.block.isabelle",
     1.6            "begin": "\\(\\*",
     1.7 -          "beginCaptures": {
     1.8 -            "0": { "name": "punctuation.definition.comment.begin.isabelle" }
     1.9 -          },
    1.10            "patterns": [{ "include": "#comment" }],
    1.11 -          "end": "\\*\\)",
    1.12 -          "endCaptures": {
    1.13 -            "0": { "name": "punctuation.definition.comment.end.isabelle" }
    1.14 -          }
    1.15 +          "end": "\\*\\)"
    1.16          }
    1.17        ]
    1.18      },
    1.19 @@ -73,14 +67,8 @@
    1.20          {
    1.21            "name": "string.quoted.other.multiline.isabelle",
    1.22            "begin": "(?:\\\\<open>|‹)",
    1.23 -          "beginCaptures": {
    1.24 -            "0": { "name": "punctuation.definition.string.begin.isabelle" }
    1.25 -          },
    1.26            "patterns": [{ "include": "#cartouche" }],
    1.27 -          "end": "(?:\\\\<close>|›)",
    1.28 -          "endCaptures": {
    1.29 -            "0": { "name": "punctuation.definition.string.end.isabelle" }
    1.30 -          }
    1.31 +          "end": "(?:\\\\<close>|›)"
    1.32          }
    1.33        ]
    1.34      }
    1.35 @@ -109,42 +97,38 @@
    1.36        "match": """ + grouped_names(keywords3) + """
    1.37      },
    1.38      {
    1.39 -      "match": "\\b\\d*\\.?\\d+\\b",
    1.40 -      "name": "constant.numeric.isabelle"
    1.41 +      "name": "constant.numeric.isabelle",
    1.42 +      "match": "\\b\\d*\\.?\\d+\\b"
    1.43      },
    1.44      {
    1.45        "name": "string.quoted.double.isabelle",
    1.46        "begin": "\"",
    1.47 -      "beginCaptures": {
    1.48 -        "0": { "name": "punctuation.definition.string.begin.isabelle" }
    1.49 -      },
    1.50        "patterns": [
    1.51          {
    1.52 -          "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """,
    1.53 -          "name": "constant.character.escape.isabelle"
    1.54 +          "name": "constant.character.escape.isabelle",
    1.55 +          "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """
    1.56          }
    1.57        ],
    1.58 -      "end": "\"",
    1.59 -      "endCaptures": {
    1.60 -        "0": { "name": "punctuation.definition.string.end.isabelle" }
    1.61 -      }
    1.62 +      "end": "\""
    1.63      },
    1.64      {
    1.65        "name": "string.quoted.backtick.isabelle",
    1.66        "begin": "`",
    1.67 -      "beginCaptures": {
    1.68 -        "0": { "name": "punctuation.definition.string.begin.isabelle" }
    1.69 -      },
    1.70        "patterns": [
    1.71          {
    1.72 -          "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """,
    1.73 -          "name": "constant.character.escape.isabelle"
    1.74 +          "name": "constant.character.escape.isabelle",
    1.75 +          "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """
    1.76          }
    1.77        ],
    1.78 -      "end": "`",
    1.79 -      "endCaptures": {
    1.80 -        "0": { "name": "punctuation.definition.string.end.isabelle" }
    1.81 -      }
    1.82 +      "end": "`"
    1.83 +    },
    1.84 +    {
    1.85 +      "name": "string.quoted.verbatim.isabelle",
    1.86 +      "begin": """ + JSON.Format("""\{\*""") + """,
    1.87 +      "patterns": [
    1.88 +        { "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ }
    1.89 +      ],
    1.90 +      "end": """ + JSON.Format("""\*\}""") + """
    1.91      }
    1.92    ]
    1.93  }