# 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": "(?:\\\\|‹)", + "beginCaptures": { + "0": { "name": "punctuation.definition.string.begin.isabelle" } + }, + "patterns": [{ "include": "#cartouche" }], + "end": "(?:\\\\|›)", + "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" } + } } ] }