# HG changeset patch
# User wenzelm
# Date 1483351186 -3600
# Node ID 34db87033abed785370d0168be95951d3f4ce3da
# Parent  0f002c15f3ab404fd3d645c928b8a636326ef40f
more syntax;
tuned;

diff -r 0f002c15f3ab -r 34db87033abe src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 10:22:59 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 10:59:46 2017 +0100
@@ -57,14 +57,8 @@
         {
           "name": "comment.block.isabelle",
           "begin": "\\(\\*",
-          "beginCaptures": {
-            "0": { "name": "punctuation.definition.comment.begin.isabelle" }
-          },
           "patterns": [{ "include": "#comment" }],
-          "end": "\\*\\)",
-          "endCaptures": {
-            "0": { "name": "punctuation.definition.comment.end.isabelle" }
-          }
+          "end": "\\*\\)"
         }
       ]
     },
@@ -73,14 +67,8 @@
         {
           "name": "string.quoted.other.multiline.isabelle",
           "begin": "(?:\\\\<open>|‹)",
-          "beginCaptures": {
-            "0": { "name": "punctuation.definition.string.begin.isabelle" }
-          },
           "patterns": [{ "include": "#cartouche" }],
-          "end": "(?:\\\\<close>|›)",
-          "endCaptures": {
-            "0": { "name": "punctuation.definition.string.end.isabelle" }
-          }
+          "end": "(?:\\\\<close>|›)"
         }
       ]
     }
@@ -109,42 +97,38 @@
       "match": """ + grouped_names(keywords3) + """
     },
     {
-      "match": "\\b\\d*\\.?\\d+\\b",
-      "name": "constant.numeric.isabelle"
+      "name": "constant.numeric.isabelle",
+      "match": "\\b\\d*\\.?\\d+\\b"
     },
     {
       "name": "string.quoted.double.isabelle",
       "begin": "\"",
-      "beginCaptures": {
-        "0": { "name": "punctuation.definition.string.begin.isabelle" }
-      },
       "patterns": [
         {
-          "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """,
-          "name": "constant.character.escape.isabelle"
+          "name": "constant.character.escape.isabelle",
+          "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """
         }
       ],
-      "end": "\"",
-      "endCaptures": {
-        "0": { "name": "punctuation.definition.string.end.isabelle" }
-      }
+      "end": "\""
     },
     {
       "name": "string.quoted.backtick.isabelle",
       "begin": "`",
-      "beginCaptures": {
-        "0": { "name": "punctuation.definition.string.begin.isabelle" }
-      },
       "patterns": [
         {
-          "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """,
-          "name": "constant.character.escape.isabelle"
+          "name": "constant.character.escape.isabelle",
+          "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """
         }
       ],
-      "end": "`",
-      "endCaptures": {
-        "0": { "name": "punctuation.definition.string.end.isabelle" }
-      }
+      "end": "`"
+    },
+    {
+      "name": "string.quoted.verbatim.isabelle",
+      "begin": """ + JSON.Format("""\{\*""") + """,
+      "patterns": [
+        { "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ }
+      ],
+      "end": """ + JSON.Format("""\*\}""") + """
     }
   ]
 }