Select by range not id in stepper

Author: Negabinary

src/haz3lcore/zipper/action/Action.re

@@ -34,6 +34,7 @@ type rel =
 [@deriving (show({with_path: false}), sexp, yojson, eq)]
 type select =
   | All
+  | PointToPoint((Point.t, Point.t))
   | Resize(move)
   | Smart(int)
   | Tile(rel)
@@ -224,6 +225,7 @@ let should_animate: t => bool =
     switch (s) {
     | Resize(_) => false
     | All
+    | PointToPoint(_)
     | Smart(_)
     | Tile(_)
     | Term(_)

src/haz3lcore/zipper/action/Perform.re

@@ -85,6 +85,13 @@ let go =
     |> return(Cant_select)
   | Select(Resize(Goal(_))) => failwith("Select not implemented for goals")
   | Select(All) => Ok(Select.all(z))
+  | Select(PointToPoint((p1, p2))) =>
+    z
+    |> Move.to_point(~measured=syntax.measured, ~goal=p1)
+    |> OptUtil.and_then(z =>
+         Select.to_point(~measured=syntax.measured, ~goal=p2, z)
+       )
+    |> return(Cant_select)
   | Select(Term(Current)) =>
     Select.current_term(
       syntax.term_data,

src/web/app/editors/result/StepperEditor.re

@@ -130,17 +130,36 @@ module View = {
 
     taken_steps(model.taken_steps)
     @ next_steps(model.next_steps, ~inject=x =>
-        Some(List.nth(model.next_steps, x)) == selected_id
-          ? signal(TakeStep(x))
-          : inject(Select(Term(Id(List.nth(model.next_steps, x), Right))))
+        {
+          open OptUtil.Syntax;
+          let+ range =
+            TermData.extreme_measures(
+              List.nth(model.next_steps, x),
+              model.editor.editor.syntax.term_data,
+              model.editor.editor.syntax.measured,
+            );
+          Some(List.nth(model.next_steps, x)) == selected_id
+            ? signal(TakeStep(x)) : inject(Select(PointToPoint(range)));
+        }
+        |> Option.value(~default=Ui_effect.Ignore)
       )
-    @ refl_steps(model.refls, ~inject=x => {
-        Some(List.nth(model.refls, x)) == selected_id
-          ? signal(Refl(x))
-          : {
-            inject(Select(Term(Id(List.nth(model.refls, x), Right))));
-          }
-      });
+    @ refl_steps(model.refls, ~inject=x =>
+        {
+          open OptUtil.Syntax;
+          let+ range =
+            TermData.extreme_measures(
+              List.nth(model.refls, x),
+              model.editor.editor.syntax.term_data,
+              model.editor.editor.syntax.measured,
+            );
+          Some(List.nth(model.refls, x)) == selected_id
+            ? signal(Refl(x))
+            : {
+              inject(Select(PointToPoint(range)));
+            };
+        }
+        |> Option.value(~default=Ui_effect.Ignore)
+      );
   };
 
   /* Steppers don't support probe dynamics - expressions shown are