implemented rollback shortcut

EugeneLoy · Jan 9, 2019 · 03b692d · 03b692d
1 parent 21f67a5
commit 03b692d
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 3 deletions.
diff --git a/coq_jupyter/kernel.js b/coq_jupyter/kernel.js
@@ -291,6 +291,23 @@
 
   return {
     onload: function() {
+      var action = {
+        icon: 'fa-step-backward',
+        cmd: 'Rollback cell',
+        help: 'Rollback cell',
+        help_index: 'zz', // TODO not shure what to set here
+        handler: function () {
+          $(".cell.selected .enabled_rollback_button, .cell.jupyter-soft-selected .enabled_rollback_button").triggerHandler("click");
+        }
+      };
+      var prefix = 'coq_jupyter';
+      var action_name = 'rollback-cell';
+
+      var jupyter = require('base/js/namespace');
+      var full_action_name = jupyter.actions.register(action, action_name, prefix);
+      jupyter.toolbar.add_buttons_group([full_action_name]);
+      jupyter.keyboard_manager.command_shortcuts.add_shortcut('Ctrl-Backspace', full_action_name);
+
       console.info('Coq kernel script loaded.');
     }
   };

diff --git a/coq_jupyter/rollback_comm.js b/coq_jupyter/rollback_comm.js
@@ -23,13 +23,19 @@ function CoqKernelRollbackComm(display_id) {
     self.rollback = function () {
         self.comm.send({ 'comm_msg_type': 'rollback' });
         $(self.button_id).prop('disabled', true);
+        $(self.button_id).removeClass("enabled_rollback_button");
     };
 
     self.handle_comm_message = function(msg) {
         if (msg.content.data.comm_msg_type === "rollback_state") {
-            $(self.output_id).toggle(!msg.content.data.rolled_back)
-            $(self.button_id).toggle(!msg.content.data.rolled_back)
-            $(self.rollback_message_id).toggle(msg.content.data.rolled_back)
+            $(self.output_id).toggle(!msg.content.data.rolled_back);
+            $(self.rollback_message_id).toggle(msg.content.data.rolled_back);
+            $(self.button_id).toggle(!msg.content.data.rolled_back);
+            if (msg.content.data.rolled_back) {
+                $(self.button_id).removeClass("enabled_rollback_button");
+            } else {
+                $(self.button_id).addClass("enabled_rollback_button");
+            }
         } else {
             console.error('Unexpected comm message: ' + JSON.stringify(msg));
         }