# HG changeset patch
# User wenzelm
# Date 1483348979 -3600
# Node ID 0f002c15f3ab404fd3d645c928b8a636326ef40f
# Parent  ba0d4829d5f14650e433e29612f1acbbd6969540
more syntax;
tuned;

diff -r ba0d4829d5f1 -r 0f002c15f3ab src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 09:41:25 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Mon Jan 02 10:22:59 2017 +0100
@@ -52,7 +52,7 @@
   "fileTypes": ["thy"],
   "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,
   "repository": {
-    "comments": {
+    "comment": {
       "patterns": [
         {
           "name": "comment.block.isabelle",
@@ -60,18 +60,37 @@
           "beginCaptures": {
             "0": { "name": "punctuation.definition.comment.begin.isabelle" }
           },
-          "patterns": [{ "include": "#comments" }],
+          "patterns": [{ "include": "#comment" }],
           "end": "\\*\\)",
           "endCaptures": {
             "0": { "name": "punctuation.definition.comment.end.isabelle" }
           }
         }
       ]
+    },
+    "cartouche": {
+      "patterns": [
+        {
+          "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" }
+          }
+        }
+      ]
     }
   },
   "patterns": [
     {
-      "include": "#comments"
+      "include": "#comment"
+    },
+    {
+      "include": "#cartouche"
     },
     {
       "name": "keyword.control.isabelle",
@@ -101,7 +120,7 @@
       },
       "patterns": [
         {
-          "match": "\\\\.",
+          "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """,
           "name": "constant.character.escape.isabelle"
         }
       ],
@@ -109,6 +128,23 @@
       "endCaptures": {
         "0": { "name": "punctuation.definition.string.end.isabelle" }
       }
+    },
+    {
+      "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"
+        }
+      ],
+      "end": "`",
+      "endCaptures": {
+        "0": { "name": "punctuation.definition.string.end.isabelle" }
+      }
     }
   ]
 }