message: Add syntax highlighting for string blocks.
diff: {"include": "#blockComment"}
  ]
  },
  + "stringBlock": {
  + "begin": "/-\"", "end": "\"-/", "name": "comment.block.string.lean",
  + "patterns": [
  + {"include": "source.lean.markdown"},
  + {"include": "#blockComment"}
  + ]
  + },
  "modDocComment": {
  "begin": "/-!", "end": "-/", "name": "comment.block.documentation.lean",
  "patterns": [
  "patterns": [
  {"include": "#dashComment"},
  {"include": "#docComment"},
  + {"include": "#stringBlock"},
  {"include": "#modDocComment"},
  {"include": "#blockComment"}
  ]
  