From c284f1ec06bbd9ed848b11befdfedae93ad6cd2c Mon Sep 17 00:00:00 2001
From: rnitta <attinyes@gmail.com>
Date: Fri, 11 Oct 2019 12:21:00 +0900
Subject: [PATCH] add a command to playpen

---
 src/theme/book.js | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/theme/book.js b/src/theme/book.js
index 263e8ad05b..c756e0d93a 100644
--- 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)
+                });
             }
         }
     }