ASTDiff: (GUI) Fix the shortcuts + enable to toggle the word wrap on …

…demand Related to tsantalis#727
pouryafard75 · May 29, 2024 · 5121927 · 5121927
1 parent 06694e4
commit 5121927
Showing 1 changed file with 33 additions and 16 deletions.
diff --git a/src/main/resources/web/dist/shortcuts.js b/src/main/resources/web/dist/shortcuts.js
@@ -18,28 +18,45 @@
  * Copyright 2011-2015 Floréal Morandat <florealm@gmail.com>
  */
 
+function toggleWordWrap() {
+    // Toggle word wrap
+    toggleEditor(window.rightEditor);
+    toggleEditor(window.leftEditor);
+    function toggleEditor(editor) {
+        if (editor) {
+            var currentWrapMode = editor.getRawOptions().wordWrap;
+            var newWrapMode = currentWrapMode === 'on' ? 'off' : 'on';
+            editor.updateOptions({wordWrap: newWrapMode});
+        }
+    }
+}
+
 $(function(){
     let popoverTriggerList = [].slice.call(document.querySelectorAll('[data-bs-toggle="popover"]'))
     let popoverList = popoverTriggerList.map(function (popoverTriggerEl) {
       return new bootstrap.Popover(popoverTriggerEl)
     })
+    $("body").keypress(function(event) {
+        if (event.altKey)
+        {
+            switch (event.code){
+                case "KeyT":
+                    $('html, body').animate({scrollTop: 0}, 100);
+                    break;
+                case "KeyB":
+                    $("html, body").animate({ scrollTop: $(document).height() }, 100);
+                    break;
+                case "KeyQ":
+                    window.location = "/quit";
+                    break;
+                case "KeyL":
+                    window.location = "/list";
+                    break;
+                case "KeyW":
+                    toggleWordWrap();
+                    break;
+            }
 
-    $("body").keypress(function (event) {
-        switch (event.which) {
-            //TODO: Disable hotkeys (temp)
-
-            // case 116:
-            //     $('html, body').animate({scrollTop: 0}, 100);
-            //     break;
-            // case 98:
-            //     $("html, body").animate({ scrollTop: $(document).height() }, 100);
-            //     break;
-            // case 113:
-            //     window.location = "/quit";
-            //     break;
-            // case 108:
-            //     window.location = "/list";
-            //     break;
         }
     });
 });