clarified menu;
authorwenzelm
Thu Jun 08 15:12:30 2017 +0200 (2017-06-08)
changeset 6604298aaeff47795
parent 66041 c49bd8bb4839
child 66043 f704c063e95d
clarified menu;
avoid non-portable ALT-mouse combination;
src/Tools/VSCode/extension/package.json
     1.1 --- a/src/Tools/VSCode/extension/package.json	Thu Jun 08 14:27:13 2017 +0200
     1.2 +++ b/src/Tools/VSCode/extension/package.json	Thu Jun 08 15:12:30 2017 +0200
     1.3 @@ -67,8 +67,12 @@
     1.4              "editor/title": [
     1.5                  {
     1.6                      "when": "editorLangId == isabelle",
     1.7 +                    "command": "isabelle.preview",
     1.8 +                    "group": "navigation"
     1.9 +                },
    1.10 +                {
    1.11 +                    "when": "editorLangId == isabelle",
    1.12                      "command": "isabelle.preview-split",
    1.13 -                    "alt": "isabelle.preview",
    1.14                      "group": "navigation"
    1.15                  },
    1.16                  {