Proof selection snapping/expansion

src/haz3lcore/derived/TermData.re

@@ -97,3 +97,29 @@ let get_term_rows =
     |> List.map(List.rev);
   (start.row, term_rows);
 };
+
+let get_root_id_using_ranges =
+    (s: Base.segment, data: t, measured: Measured.t): option(Id.t) => {
+  let id_and_ranges =
+    s
+    |> List.filter_map((p: Piece.t) => {
+         let id = Piece.id(p);
+         let range_opt = extreme_measures(id, data, measured);
+         Option.map(r => (id, r), range_opt);
+       });
+  ListUtil.max(
+    ((_, (start1, end1)), (_, (start2, end2))) =>
+      switch (Point.comp(start1, start2)) {
+      | Under => Direction.Left
+      | Over => Direction.Right
+      | Exact =>
+        switch (Point.comp(end1, end2)) {
+        | Under => Direction.Right
+        | Over => Direction.Left
+        | Exact => Direction.Right
+        }
+      },
+    id_and_ranges,
+  )
+  |> Option.map(fst);
+};

src/util/ListUtil.re

@@ -587,3 +587,21 @@ let assoc_update = (key, f, assoc) => {
 
 let remove_assoc = (key, assoc) =>
   List.filter(((k, _)) => k != key, assoc);
+
+let max = (cmp: ('a, 'a) => Direction.t, xs: list('a)): option('a) => {
+  switch (xs) {
+  | [] => None
+  | [x, ...xs] =>
+    Some(
+      List.fold_left(
+        (current_max, candidate) =>
+          switch (cmp(current_max, candidate)) {
+          | Left => current_max
+          | Right => candidate
+          },
+        x,
+        xs,
+      ),
+    )
+  };
+};

src/web/app/editors/code/CodeEditable.re

@@ -227,14 +227,24 @@ module View = {
 
   module MouseState = Pointer.MkState();
 
-  let deco = (~syntax: CachedSyntax.t, ~z: Zipper.t, ~globals: Globals.t) => [
+  let deco =
+      (
+        ~expand_selection=false,
+        ~syntax: CachedSyntax.t,
+        ~globals: Globals.t,
+        z: Zipper.t,
+      ) => [
     CaretDec.view(
       ~measured=syntax.measured,
       ~font_metrics=globals.font_metrics,
       z,
     ),
     Arms.Indicated.term(~font_metrics=globals.font_metrics, ~syntax, z),
-    Highlight.selection(
+    (
+      expand_selection
+        ? Highlight.selection_expanded(~term_data=syntax.term_data)
+        : Highlight.selection
+    )(
       ~measured=syntax.measured,
       ~shape_map=syntax.shape_map,
       ~font_metrics=globals.font_metrics,
@@ -261,6 +271,7 @@ module View = {
         ~selected: bool,
         ~overlays: list(Node.t)=[],
         ~dynamics: Language.Dynamics.Map.t,
+        ~expand_selection=?,
         model: Model.t,
       ) => {
     /* Sync document-level click listener for closing context menu */
@@ -271,9 +282,10 @@ module View = {
     let edit_decos =
       selected
         ? deco(
-            ~z=model.editor.state.zipper,
+            ~expand_selection?,
             ~syntax=model.editor.syntax,
             ~globals,
+            model.editor.state.zipper,
           )
           @ [
             Arms.Refractors.all(

src/web/app/editors/decoration/Highlight.re

@@ -215,6 +215,50 @@ let selection =
     ),
   );
 
+// Explands selection to make it a subtree of the exp
+let selection_expanded =
+    (
+      ~measured: Measured.t,
+      ~shape_map: ProjectorCore.Shape.Map.t,
+      ~font_metrics: FontMetrics.t,
+      ~term_data: TermData.t,
+      z: Zipper.t,
+    ) =>
+  div_c(
+    "selects",
+    switch (
+      TermData.get_root_id_using_ranges(
+        z.selection.content,
+        term_data,
+        measured,
+      )
+    ) {
+    | None => []
+    | Some(id) =>
+      let seg = TermData.segment(id, term_data);
+      switch (seg) {
+      | None => []
+      | Some(seg) =>
+        of_segment(
+          ~measured,
+          ~shape_map,
+          ~font_metrics,
+          ~shape_init=Some(fst(Siblings.shapes(z.relatives.siblings))),
+          ~clss=["selected-expanded", Selection.buffer_cls(z.selection)],
+          seg,
+        )
+        @ of_segment(
+            ~measured,
+            ~shape_map,
+            ~font_metrics,
+            ~shape_init=Some(fst(Siblings.shapes(z.relatives.siblings))),
+            ~clss=["selected", Selection.buffer_cls(z.selection)],
+            z.selection.content,
+          )
+      };
+    },
+  );
+
 let indicated_refractor =
     (
       ~measured: Measured.t,

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

@@ -176,6 +176,7 @@ module View = {
         model: Model.t,
       ) => {
     CodeSelectable.View.view(
+      ~expand_selection=true,
       ~dynamics=Language.Dynamics.Map.empty,
       ~signal=
         fun

src/web/app/editors/stepper/MissingStep.re

@@ -162,16 +162,19 @@ module Update = {
       // hacky way to get a currently-selected id
       {
         let editor: CodeSelectable.Model.t = editor |> Calc.get_value;
-        try({
-          let zipper = editor.editor.state.zipper;
-          let selection = zipper.selection.content;
-          let skel = Segment.skel(selection);
-          let root = Skel.root(skel);
-          let idx = Aba.first_a(root);
-          let piece = List.nth(selection, idx);
-          let id = Piece.id(piece);
-          Some(id);
-        }) {
+        try(
+          {
+            open OptUtil.Syntax;
+            let zipper = editor.editor.state.zipper;
+            let* id =
+              TermData.get_root_id_using_ranges(
+                zipper.selection.content,
+                editor.editor.syntax.term_data,
+                editor.editor.syntax.measured,
+              );
+            Some(id);
+          }
+        ) {
         | _ => None
         };
       }

src/web/www/style/editor.css

@@ -222,6 +222,16 @@ svg.shard.selected > path {
   stroke: var(--shard-selected);
 }
 
+svg.shard.selected-expanded {
+  z-index: var(--select-z);
+  filter: drop-shadow(2px 2px 2px var(--shadow-selected));
+}
+svg.shard.selected-expanded > path {
+  fill: var(--shard-selected-expanded);
+  stroke-width: 0.5px;
+  stroke: var(--shard-selected-expanded);
+}
+
 .errors .errors-piece svg.shard {
   z-index: var(--err-hole-z);
   filter: none;

src/web/www/style/variables.css

@@ -108,6 +108,7 @@
   --shard-typ: var(--shard-caret-typ);
   --shard-tpat: var(--shard-caret-tpat);
   --shard-selected: var(--Y1);
+  --shard-selected-expanded: var(--Y0);
   --shard-buffer: var(--T1);
   --shard_projector: var(--T2);
   --shard-rul: var(--shard-exp);