Fixed problems with attempting to place caret on recently deleted edi…

…tor following title-editor branch
hazelgrove · Nov 25, 2024 · 9e7900d · 9e7900d
1 parent 0b040a5
commit 9e7900d
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 12 deletions.
diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
@@ -211,7 +211,7 @@ module F = (ExerciseEnv: ExerciseEnv) => {
               tests: editor,
               provided: new_prov_test,
             },
-          } /* Set 'provided' to 1 if editing_test_val_rep is true */
+          },
         }
         : {
           ...state,
@@ -573,11 +573,10 @@ module F = (ExerciseEnv: ExerciseEnv) => {
             index < length - 1 ? index + 1 : index - 1,
           ).
             impl
-        : state.eds.your_tests.tests;
+        : state.eds.your_impl;
     let pos =
       length > 1
-        ? HiddenBugs(index < length - 1 ? index : index - 1)
-        : YourTestsValidation;
+        ? HiddenBugs(index < length - 1 ? index : index - 1) : YourImpl;
     let new_state = {
       pos,
       eds: {

diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re
@@ -42,14 +42,8 @@ let apply = (model, action, ~schedule_action): Model.t => {
       last_edit_action := JsUtil.timestamp();
       edit_action_applied := true;
     };
-    let old_scroll = scroll_to_caret.contents;
     if (Update.should_scroll_to_caret(action)) {
       scroll_to_caret := true;
-      Printf.printf(
-        "DEBUG: Scroll set to true for action: %s (was: %b)\n",
-        UpdateAction.show(action),
-        old_scroll,
-      );
     };
     last_edit_action := JsUtil.timestamp();
     switch (

diff --git a/src/haz3lweb/Main.rei b/src/haz3lweb/Main.rei
diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
@@ -360,7 +360,14 @@ let wrong_impl_caption = (~inject, sub: string, n: int) => {
     [
       caption("", ~rest=sub),
       div(
-        ~attrs=[Attr.class_("instructor-edit-icon")],
+        ~attrs=[
+          Attr.class_("instructor-edit-icon"),
+          Attr.on_mousedown(_ =>
+            Virtual_dom.Vdom.Effect.(
+              Many([Prevent_default, Stop_propagation])
+            )
+          ),
+        ],
         [
           Widgets.button(
             Icons.delete,