From 03b692d1d9f7787d6cfb192a36b03236b778c946 Mon Sep 17 00:00:00 2001
From: Eugene Loy <eugeny.loy@gmail.com>
Date: Wed, 9 Jan 2019 15:04:23 +0200
Subject: [PATCH] implemented rollback shortcut

---
 coq_jupyter/kernel.js        | 17 +++++++++++++++++
 coq_jupyter/rollback_comm.js | 12 +++++++++---
 2 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/coq_jupyter/kernel.js b/coq_jupyter/kernel.js
index e5debc3..0c7ce14 100644
--- 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
index 0dbe5a8..68f3d8e 100644
--- 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));
         }