diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index d1394f76af..b72353f632 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -94,10 +94,6 @@ module Meta = { | Move(Local(Up | Down)) | Select(Resize(Local(Up | Down))) => col_target | _ => - // switch (Indicated.index(z_projected)) { - // | Some(i) => print_endline("indicated_id:" ++ Id.show(i)) - // | None => print_endline("no indicated_id") - // }; print_endline("Editor.next.caret_point"); Zipper.caret_point(measured_projected, z_projected).col; }; diff --git a/src/haz3lcore/zipper/action/Indicated.re b/src/haz3lcore/zipper/action/Indicated.re index f9e3a3fcd4..e70a77a014 100644 --- a/src/haz3lcore/zipper/action/Indicated.re +++ b/src/haz3lcore/zipper/action/Indicated.re @@ -7,20 +7,15 @@ type relation = | Sibling; let piece' = - (~no_ws: bool, ~ign: Piece.t => bool, ~trim_secondary=false, z: Zipper.t) + (~no_ws: bool, ~ign: Piece.t => bool, z: Zipper.t) : option((Piece.t, Direction.t, relation)) => { - let sibs = - trim_secondary - ? sibs_with_sel(z) |> Siblings.trim_secondary : sibs_with_sel(z); /* Returns the piece currently indicated (if any) and which side of that piece the caret is on. We favor indicating the piece to the (R)ight, but may end up indicating the (P)arent or the (L)eft. We don't indicate secondary tiles. This function ignores whether or not there is a selection so this can be used to get the caret direction, but the caller shouldn't indicate if there's a selection */ - switch (Siblings.neighbors(sibs), parent(z)) { - /* Non-empty selection => no indication */ - //| _ when z.selection.content != [] => None + switch (Siblings.neighbors(sibs_with_sel(z)), parent(z)) { /* Empty syntax => no indication */ | ((None, None), None) => None /* L not secondary, R is secondary => indicate L */ @@ -85,8 +80,7 @@ let shard_index = (z: Zipper.t): option(int) => } }; -let for_index = - piece'(~no_ws=false, ~ign=Piece.is_secondary, ~trim_secondary=false); +let for_index = piece'(~no_ws=false, ~ign=Piece.is_secondary); let index = (z: Zipper.t): option(Id.t) => switch (for_index(z)) { @@ -101,9 +95,7 @@ let ci_of = (z: Zipper.t, info_map: Statics.Map.t): option(Statics.Info.t) => * Secondary. But if this doesn't succeed, then we create a 'virtual' * info map entry representing the Secondary notation, which takes on * some of the semantic context of a nearby 'proxy' term */ - switch ( - piece'(~no_ws=true, ~ign=Piece.is_secondary, ~trim_secondary=false, z) - ) { + switch (piece'(~no_ws=true, ~ign=Piece.is_secondary, z)) { | Some((p, _, _)) => Id.Map.find_opt(Piece.id(p), info_map) | None => let sibs = sibs_with_sel(z); diff --git a/src/haz3lweb/view/Deco.re b/src/haz3lweb/view/Deco.re index 76b22c282d..ff973d3cd1 100644 --- a/src/haz3lweb/view/Deco.re +++ b/src/haz3lweb/view/Deco.re @@ -43,35 +43,27 @@ module Deco = (start_shape: Nib.Shape.t, p: Piece.t) : (Nib.Shape.t, list(option(shard_data))) => { let shard_data = - try( - switch (p) { - | Tile(t) => sel_of_tile(~start_shape, t) - | Grout(g) => [ - Some( - sel_shard_svg( - ~start_shape, - Measured.find_g(~msg="Deco.sel_of_piece", g, M.map), - p, - ), + switch (p) { + | Tile(t) => sel_of_tile(~start_shape, t) + | Grout(g) => [ + Some( + sel_shard_svg( + ~start_shape, + Measured.find_g(~msg="Deco.sel_of_piece", g, M.map), + p, ), - ] - | Secondary(w) when Secondary.is_linebreak(w) => [None] - | Secondary(w) => [ - Some( - sel_shard_svg( - ~start_shape, - Measured.find_w(~msg="Deco.sel_of_piece", w, M.map), - p, - ), + ), + ] + | Secondary(w) when Secondary.is_linebreak(w) => [None] + | Secondary(w) => [ + Some( + sel_shard_svg( + ~start_shape, + Measured.find_w(~msg="Deco.sel_of_piece", w, M.map), + p, ), - ] - } - ) { - | _ => - print_endline("PROJECTOR CRASH: sel_of_piece"); - //TODO(andrew): relax. this is the case when tiles are missing - //measured info due to being hidden by a projector - []; + ), + ] }; let start_shape = switch (Piece.nibs(p)) { diff --git a/src/haz3lweb/view/ProjectorsView.re b/src/haz3lweb/view/ProjectorsView.re index e596d7de51..8f9089bf5b 100644 --- a/src/haz3lweb/view/ProjectorsView.re +++ b/src/haz3lweb/view/ProjectorsView.re @@ -10,16 +10,6 @@ let stop_mousedown_propagation = Virtual_dom.Vdom.Effect.Ignore; }); -let simple_shard = (~font_metrics, ~measurement: Measured.measurement) => - PieceDec.simple_shard( - ~absolute=false, - ~font_metrics, - ~shapes=(Convex, Convex), - ~path_cls=[], - ~base_cls=[], - measurement, - ); - let fold_view = (id, clss, ~font_metrics, ~inject, ~measurement) => div( ~attr= @@ -31,7 +21,7 @@ let fold_view = (id, clss, ~font_metrics, ~inject, ~measurement) => ), DecUtil.abs_style(measurement, ~font_metrics), ]), - [text("⋱"), simple_shard(~font_metrics, ~measurement)], + [text("⋱"), PieceDec.convex_shard(~font_metrics, ~measurement)], ); let infer_view = @@ -53,7 +43,10 @@ let infer_view = ), DecUtil.abs_style(measurement, ~font_metrics), ]), - [Type.view(expected_ty), simple_shard(~font_metrics, ~measurement)], + [ + Type.view(expected_ty), + PieceDec.convex_shard(~font_metrics, ~measurement), + ], ); let display_ty = (expected_ty: option(Typ.t)): Typ.t => diff --git a/src/haz3lweb/view/dec/PieceDec.re b/src/haz3lweb/view/dec/PieceDec.re index bd14945d10..15f5eadeac 100644 --- a/src/haz3lweb/view/dec/PieceDec.re +++ b/src/haz3lweb/view/dec/PieceDec.re @@ -59,6 +59,19 @@ let simple_shard = simple_shard_path(shapes, measurement.last.col - measurement.origin.col), ); +let relative_shard = + (~font_metrics, ~shapes, ~measurement: Measured.measurement) => + simple_shard( + ~absolute=false, + ~font_metrics, + ~shapes, + ~path_cls=[], + ~base_cls=[], + measurement, + ); + +let convex_shard = relative_shard(~shapes=(Convex, Convex)); + let simple_shard_selected = (~font_metrics, ~shapes, ~measurement: Measured.measurement, ~buffer): t => { let path_cls = [