message: Enable markdown highlighting in all the comments!
diff: "dashComment": {
  "begin": "(--)", "end": "$",
  "beginCaptures": {"0": {"name": "punctuation.definition.comment.lean"}},
  - "name": "comment.line.double-dash.lean"
  + "name": "comment.line.double-dash.lean",
  + "patterns": [
  + {"include": "source.lean.markdown"}
  + ]
  },
  "docComment": {
  "begin": "/--", "end": "-/", "name": "comment.block.documentation.lean",
  },
  "blockComment": {
  "begin": "/-", "end": "-/", "name": "comment.block.lean",
  - "patterns": [{"include": "#blockComment"}]
  + "patterns": [
  + {"include": "source.lean.markdown"},
  + {"include": "#blockComment"}
  + ]
  },
  "comments": {
  "patterns": [
  