Ctrl + d keyboard shortcut interferes with macOS functionality

[terasakisatoshi]

I prefer to use Ctrl-P/N/F/B/D/K/Y/D/A/E on macOS to control the cursor on text. On Pluto notebook, It seems Ctrl-P/N/F/B/K/A/E works as described in Document shortcuts section of Mac keyboard shortcuts: https://support.apple.com/en-us/HT201236.

Unfortunately Ctrl-D does not work as Control-D: Delete the character to the right of the insertion point..

Since line in KeyboardShortcuts.js tries to replace Ctrl-blah-blah in with Cmd-blah-blah in keymap, one may think this is fine.

Pluto.jl/frontend/common/KeyboardShortcuts.js

Line 14 in cd7c123

keymap_with_cmd[key.replace(/Ctrl/g, "Cmd")] = handler

However, this lines assigns Ctrl-D shortcut to do something (selecting some words ???)

Pluto.jl/frontend/components/CellInput.js

Lines 151 to 162 in 28615ad

	keys["Ctrl-D"] = () => {
	if (cm.somethingSelected()) {
	const sels = cm.getSelections()
	if (all_equal(sels)) {
	// TODO
	}
	} else {
	const cursor = cm.getCursor()
	const token = cm.getTokenAt(cursor)
	cm.setSelection({ line: cursor.line, ch: token.start }, { line: cursor.line, ch: token.end })
	}
	}

If I remove this lines above, I can use Ctrl-D to delete the character to the right, which is what I expect on macOS.

Note that if one would like to use Ctrl-D functionality that Pluto.jl provides on macOS, one only have to do use Cmd+D (due to this line

Pluto.jl/frontend/common/KeyboardShortcuts.js

Line 14 in cd7c123

keymap_with_cmd[key.replace(/Ctrl/g, "Cmd")] = handler

) .

Do we need insert conditional branch something like ?

if (!is_mac_keyboard){
  keys["Ctrl-D"] = () => {
  // do something
  }
}

Any thoughts about this issue ?

[terasakisatoshi]

using delete to remove Ctrl-... key from keymap_with_cmd works.

export let map_cmd_to_ctrl_on_mac = (keymap) => {
    if (!is_mac_keyboard) {
        return keymap
    }

    let keymap_with_cmd = { ...keymap }
    for (let [key, handler] of Object.entries(keymap)) {
        keymap_with_cmd[key.replace(/Ctrl/g, "Cmd")] = handler
        delete keymap_with_cmd[key] // delete Ctrl-blah-blah e.g. Ctrl-D or Ctrl-M etc ...
    }
    return keymap_with_cmd
}

[fonsp]

Thanks! Feel free to make a PR, but note that removing the Ctrl- shortcuts will break other shortcuts, e.g. Ctrl-M for md""" (i am not sure if there are others), so take that into account.

[likanzhan]

As Ctrl + d has been removed, is there a shortcut to stop the Pluto in the terminal? Thanks