message: Remove toggleSticky and copytocomment from editor taskbar.
  This is because they are now shown in the infoview directly.
  The commands should still work.
diff: "command": "lean.infoView.displayGoal",
  "when": "infoViewFocused",
  "group": "navigation@2"
  - },
  - {
  - "command": "lean.infoView.copyToComment",
  - "when": "editorLangId == lean",
  - "group": "navigation@3"
  - },
  - {
  - "command": "lean.infoView.toggleStickyPosition",
  - "when": "editorLangId == lean",
  - "group": "navigation@4"
  }
  ]
  }
  