control.js 2.3 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899
  1. function next_uncovered(selector, reverse, scroll_selector) {
  2. function visit_element(element) {
  3. element.classList.add("seen");
  4. element.classList.add("selected");
  5. if (!scroll_selector) {
  6. scroll_selector = "tr:has(.selected) td.line-number"
  7. }
  8. const scroll_to = document.querySelector(scroll_selector);
  9. if (scroll_to) {
  10. scroll_to.scrollIntoView({behavior: "smooth", block: "center", inline: "end"});
  11. }
  12. }
  13. function select_one() {
  14. if (!reverse) {
  15. const previously_selected = document.querySelector(".selected");
  16. if (previously_selected) {
  17. previously_selected.classList.remove("selected");
  18. }
  19. return document.querySelector(selector + ":not(.seen)");
  20. } else {
  21. const previously_selected = document.querySelector(".selected");
  22. if (previously_selected) {
  23. previously_selected.classList.remove("selected");
  24. previously_selected.classList.remove("seen");
  25. }
  26. const nodes = document.querySelectorAll(selector + ".seen");
  27. if (nodes) {
  28. const last = nodes[nodes.length - 1]; // last
  29. return last;
  30. } else {
  31. return undefined;
  32. }
  33. }
  34. }
  35. function reset_all() {
  36. if (!reverse) {
  37. const all_seen = document.querySelectorAll(selector + ".seen");
  38. if (all_seen) {
  39. all_seen.forEach(e => e.classList.remove("seen"));
  40. }
  41. } else {
  42. const all_seen = document.querySelectorAll(selector + ":not(.seen)");
  43. if (all_seen) {
  44. all_seen.forEach(e => e.classList.add("seen"));
  45. }
  46. }
  47. }
  48. const uncovered = select_one();
  49. if (uncovered) {
  50. visit_element(uncovered);
  51. } else {
  52. reset_all();
  53. const uncovered = select_one();
  54. if (uncovered) {
  55. visit_element(uncovered);
  56. }
  57. }
  58. }
  59. function next_line(reverse) {
  60. next_uncovered("td.uncovered-line", reverse)
  61. }
  62. function next_region(reverse) {
  63. next_uncovered("span.red.region", reverse);
  64. }
  65. function next_branch(reverse) {
  66. next_uncovered("span.red.branch", reverse);
  67. }
  68. document.addEventListener("keypress", function(event) {
  69. const reverse = event.shiftKey;
  70. if (event.code == "KeyL") {
  71. next_line(reverse);
  72. }
  73. if (event.code == "KeyB") {
  74. next_branch(reverse);
  75. }
  76. if (event.code == "KeyR") {
  77. next_region(reverse);
  78. }
  79. });