diff --git a/src/haz3lcore/derived/TermData.re b/src/haz3lcore/derived/TermData.re index 38e26e8c99..9f94fff8eb 100644 --- a/src/haz3lcore/derived/TermData.re +++ b/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); +}; diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index f583a566f3..a41b231447 100644 --- a/src/util/ListUtil.re +++ b/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, + ), + ) + }; +}; diff --git a/src/web/app/editors/code/CodeEditable.re b/src/web/app/editors/code/CodeEditable.re index 288cf02418..64994b983e 100644 --- a/src/web/app/editors/code/CodeEditable.re +++ b/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( diff --git a/src/web/app/editors/decoration/Highlight.re b/src/web/app/editors/decoration/Highlight.re index f700ad5d47..b16ef1f387 100644 --- a/src/web/app/editors/decoration/Highlight.re +++ b/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, diff --git a/src/web/app/editors/result/StepperEditor.re b/src/web/app/editors/result/StepperEditor.re index 0361bc8a7f..aa6f551dab 100644 --- a/src/web/app/editors/result/StepperEditor.re +++ b/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 diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index a19fbdcf1f..a88b7ac3f0 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/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 }; } diff --git a/src/web/www/style/editor.css b/src/web/www/style/editor.css index 56f7f0f70a..5fc37870b4 100644 --- a/src/web/www/style/editor.css +++ b/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; diff --git a/src/web/www/style/variables.css b/src/web/www/style/variables.css index 395aeffe97..a65ce6f919 100644 --- a/src/web/www/style/variables.css +++ b/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);