add a command to playpen (#1066)

rust-lang · Oct 11, 2019 · 01e5030 · 01e5030
1 parent 2b3304c
commit 01e5030
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/theme/book.js b/src/theme/book.js
@@ -55,6 +55,15 @@ function playpen_text(playpen) {
                 editor.addEventListener("change", function (e) {
                     update_play_button(playpen_block, playground_crates);
                 });
+                // add Ctrl-Enter command to execute rust code
+                editor.commands.addCommand({
+                    name: "run",
+                    bindKey: {
+                        win: "Ctrl-Enter",
+                        mac: "Ctrl-Enter"
+                    },
+                    exec: _editor => run_rust_code(playpen_block)
+                });
             }
         }
     }