Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

code folding #1113

Closed
wants to merge 34 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
e8e0f1e
create fold button
gensofubi Sep 19, 2023
c3a9812
add the checkbox into code view
gensofubi Sep 19, 2023
72cb6ee
fix tile indication position
gensofubi Sep 21, 2023
b63e74b
don't show checkbox on incomplete keyword or backpack
gensofubi Sep 22, 2023
3d2756a
hide folded texts
gensofubi Oct 7, 2023
53a6993
rename fold
gensofubi Oct 7, 2023
d0f24aa
replace folded codes with <...>
gensofubi Oct 7, 2023
743fefc
remove collapsed holes
gensofubi Oct 7, 2023
f2a49e6
restore the holes in pattern
gensofubi Oct 7, 2023
50486f2
use performaction, history partially corrected
gensofubi Oct 7, 2023
f2c287a
measured for folded codes
gensofubi Oct 7, 2023
efa7feb
add default value for folded in measured
gensofubi Oct 7, 2023
959772c
compression to fix position in 'in' and moving up and down
gensofubi Oct 14, 2023
63d470f
Merge branch 'haz3l-module' into haz3l-module-view
gensofubi Oct 14, 2023
1eefcbd
disallowing moving into folded codes by direction keys
gensofubi Oct 15, 2023
cf00d6e
extract the checkbox out of codes and move it to the side
gensofubi Oct 22, 2023
d6faafb
revert the indent for checkboxs in measured
gensofubi Oct 22, 2023
6541164
move to begin of line when fold,(Forced movement to resolve delays in…
gensofubi Oct 27, 2023
0039263
change move goal to origin of the folding module
gensofubi Oct 27, 2023
1c5334e
stop using checkbox, change the appearance of button
gensofubi Oct 27, 2023
939f5bb
use actual html button
gensofubi Oct 27, 2023
e50596f
fundamentally solved the delay in update
gensofubi Oct 28, 2023
bca8eb8
remove redundant move
gensofubi Oct 28, 2023
b8cde4b
split action fold and unfold
gensofubi Oct 28, 2023
bf89094
fold using keyboard ctrl+shift+[]
gensofubi Oct 28, 2023
928304b
combine fold and move (for better undo)
gensofubi Nov 5, 2023
54b171d
find upper level fold if current is folded
gensofubi Nov 5, 2023
4a8f5aa
display on hovering, css change
gensofubi Nov 6, 2023
a7c9849
some random conspicuous color
gensofubi Nov 6, 2023
b098bb4
position adjustment
gensofubi Nov 6, 2023
118c2f4
Merge branch 'haz3l-module' into haz3l-module-view
gensofubi Nov 12, 2023
e106f78
icon view adjustment
gensofubi Nov 13, 2023
122ad00
position fix
gensofubi Nov 25, 2023
abadefa
Merge branch 'haz3l-module' into haz3l-module-view
gensofubi Nov 27, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 41 additions & 19 deletions src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
Expand Up @@ -267,7 +267,8 @@ let is_indented_map = (seg: Segment.t) => {
go(seg);
};

let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
let of_segment =
(~old: t=empty, ~touched=Touched.empty, ~folded=[], seg: Segment.t): t => {
let is_indented = is_indented_map(seg);

// recursive across seg's bidelimited containers
Expand All @@ -276,6 +277,8 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
~map,
~container_indent: abs_indent=0,
~origin=Point.zero,
~compress=false,
~outermost=false,
seg: Segment.t,
)
: (Point.t, t) => {
Expand Down Expand Up @@ -319,9 +322,17 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
);
(origin, map);
| [hd, ...tl] =>
let fold = (origin: Point.t, last: Point.t) => {
let folded_last =
switch (tl) {
| [] when outermost => Point.{...origin, col: origin.col + 7}
| _ => origin
};
compress ? folded_last : last;
};
let (contained_indent, origin, map) =
switch (hd) {
| Secondary(w) when Secondary.is_linebreak(w) =>
| Secondary(w) when Secondary.is_linebreak(w) && !compress =>
let row_indent = container_indent + contained_indent;
let indent =
if (Segment.sameline_secondary(tl)) {
Expand Down Expand Up @@ -352,37 +363,48 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
| Secondary(w) =>
let wspace_length =
Unicode.length(Secondary.get_string(w.content));
let last = {...origin, col: origin.col + wspace_length};
let last =
{...origin, col: origin.col + wspace_length} |> fold(origin);
let map = map |> add_w(w, {origin, last});
(contained_indent, last, map);
| Grout(g) =>
let last = {...origin, col: origin.col + 1};
let last = {...origin, col: origin.col + 1} |> fold(origin);
let map = map |> add_g(g, {origin, last});
(contained_indent, last, map);
| Tile(t) =>
let token = List.nth(t.label);
let add_shard = (origin, shard, map) => {
let add_shard = (origin, shard, map, count) => {
let last =
Point.{
...origin,
col: origin.col + String.length(token(shard)),
};
}
|> fold(origin);
let map = map |> add_s(t.id, shard, {origin, last});
(last, map);
(last, map, count + 1);
};
let (last, map) =
let (last, map, _) =
Aba.mk(t.shards, t.children)
|> Aba.fold_left(
shard => add_shard(origin, shard, map),
((origin, map), child, shard) => {
shard => add_shard(origin, shard, map, 0),
((origin, map, count), child, shard) => {
let in_folded = List.mem(t.id, folded) && count == 2;
let (child_last, child_map) =
go_nested(
~map,
~container_indent=container_indent + contained_indent,
~origin,
~compress=compress || in_folded,
~outermost=in_folded && !compress,
child,
);
add_shard(child_last, shard, child_map);
// let child_last =
// if (List.mem(t.id, folded_list) && count == 2) {
// Point.{...origin, col: origin.col + 7};
// } else {
// child_last;
// };
add_shard(child_last, shard, child_map, count);
},
);
(contained_indent, last, map);
Expand All @@ -407,27 +429,27 @@ let length = (seg: Segment.t, map: t): int =>
last.last.col - first.origin.col;
};

let segment_origin = (seg: Segment.t): option(Point.t) =>
let segment_origin = (~folded=[], seg: Segment.t): option(Point.t) =>
Option.map(
first => find_p(first, of_segment(seg)).origin,
first => find_p(first, of_segment(seg, ~folded)).origin,
ListUtil.hd_opt(seg),
);

let segment_last = (seg: Segment.t): option(Point.t) =>
let segment_last = (~folded=[], seg: Segment.t): option(Point.t) =>
Option.map(
last => find_p(last, of_segment(seg)).last,
last => find_p(last, of_segment(seg, ~folded)).last,
ListUtil.last_opt(seg),
);

let segment_height = (seg: Segment.t) =>
switch (segment_last(seg), segment_origin(seg)) {
let segment_height = (~folded=[], seg: Segment.t) =>
switch (segment_last(seg, ~folded), segment_origin(seg, ~folded)) {
| (Some(last), Some(first)) => 1 + last.row - first.row
| _ => 0
};

let segment_width = (seg: Segment.t): int =>
let segment_width = (~folded=[], seg: Segment.t): int =>
IntMap.fold(
(_, {max_col, _}: Rows.shape, acc) => max(max_col, acc),
of_segment(seg).rows,
of_segment(seg, ~folded).rows,
0,
);
10 changes: 10 additions & 0 deletions src/haz3lcore/statics/Module.re
Original file line number Diff line number Diff line change
Expand Up @@ -50,3 +50,13 @@ let rec get_module =
| _ => None
};
};

let foldable = (tile: Tile.t) =>
tile.label == ["module", "=", "in"]
&& List.length(tile.shards) == List.length(tile.label);
let foldable_anc = (tile: Ancestor.t) => {
let (s1, s2) = tile.shards;
let shard_length = List.length(s1) + List.length(s2);
tile.label == ["module", "=", "in"]
&& shard_length == List.length(tile.label);
};
15 changes: 12 additions & 3 deletions src/haz3lcore/zipper/Editor.re
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module Meta = {
measured: Measured.t,
term_ranges: TermRanges.t,
col_target: int,
folded: list(Id.t),
};

let init = (z: Zipper.t) => {
Expand All @@ -16,6 +17,7 @@ module Meta = {
measured: Measured.of_segment(unselected),
term_ranges: TermRanges.mk(unselected),
col_target: 0,
folded: [],
};
};

Expand All @@ -42,18 +44,25 @@ module Meta = {

let next =
(~effects: list(Effect.t)=[], a: Action.t, z: Zipper.t, meta: t): t => {
let {touched, measured, col_target, _} = meta;
let {touched, measured, col_target, folded, _} = meta;
let touched = Touched.update(Time.tick(), effects, touched);
let unselected = Zipper.unselect_and_zip(z);
let measured = Measured.of_segment(~touched, ~old=measured, unselected);
let folded =
switch (a) {
| Fold(id) => [id, ...folded]
| Unfold(id) => List.filter(x => x !== id, folded)
| _ => folded
};
let measured =
Measured.of_segment(~touched, ~old=measured, unselected, ~folded);
let term_ranges = TermRanges.mk(unselected);
let col_target =
switch (a) {
| Move(Local(Up | Down))
| Select(Resize(Local(Up | Down))) => col_target
| _ => Zipper.caret_point(measured, z).col
};
{touched, measured, term_ranges, col_target};
{touched, measured, term_ranges, col_target, folded};
};
};

Expand Down
2 changes: 2 additions & 0 deletions src/haz3lcore/zipper/action/Action.re
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ type t =
| Insert(string)
| RotateBackpack
| MoveToBackpackTarget(planar)
| Fold(Id.t)
| Unfold(Id.t)
| Pick_up
| Put_down;

Expand Down
73 changes: 54 additions & 19 deletions src/haz3lcore/zipper/action/Move.re
Original file line number Diff line number Diff line change
Expand Up @@ -73,23 +73,58 @@ module Make = (M: Editor.Meta.S) => {
let inner_end = (d, d_init, c_max, z) =>
z |> Zipper.set_caret(Inner(d_init, c_max)) |> Zipper.move(d);

let primary = (chunkiness: chunkiness, d: Direction.t, z: t): option(t) => {
switch (d, z.caret, neighbor_movability(chunkiness, z)) {
let can_pass_fold =
(
folded,
d: Direction.t,
{relatives: {ancestors, siblings: (l_sib, r_sib)}, _}: t,
) => {
switch (d, ancestors) {
| (Left, [({id, children: (l_kids, _), _}, _), ..._])
when List.mem(id, folded) && List.length(l_kids) == 1 && l_sib != [] =>
Some(id)
| (Right, [({id, children: (l_kids, _), _}, _), ..._])
when List.mem(id, folded) && List.length(l_kids) == 1 && r_sib != [] =>
Some(id)
| _ => None
};
};
let rec pass_fold = (d: Direction.t, z: t, target_id) => {
switch (d, z.relatives.siblings, z.relatives.ancestors) {
| (Left, ([], _), [({id, _}, _), ..._])
| (Right, (_, []), [({id, _}, _), ..._]) when id == target_id =>
Some(z)
| _ =>
let* z = Zipper.move(d, z);
pass_fold(d, z, target_id);
};
};

let primary =
(~folded=[], chunkiness: chunkiness, d: Direction.t, z: t): option(t) => {
switch (
d,
z.caret,
neighbor_movability(chunkiness, z),
can_pass_fold(folded, d, z),
) {
/* this case maybe shouldn't be necessary but currently covers an edge
(select an open parens to left of a multichar token and press left) */
| _ when z.selection.content != [] => pop_move(d, z)
| (Left, Outer, (CanEnter(dlm, c_max), _)) =>
| (Left, Outer, _, Some(target_id)) => pass_fold(d, z, target_id)
| (Left, Outer, (CanEnter(dlm, c_max), _), _) =>
inner_end(d, dlm, c_max, z)
| (Left, Outer, _) => Zipper.move(d, z)
| (Left, Inner(_), _) when chunkiness == ByToken => pop_out(z)
| (Left, Inner(_), _) =>
| (Left, Outer, _, _) => Zipper.move(d, z)
| (Left, Inner(_), _, _) when chunkiness == ByToken => pop_out(z)
| (Left, Inner(_), _, _) =>
Some(Zipper.update_caret(Zipper.Caret.decrement, z))
| (Right, Outer, (_, CanEnter(d_init, _))) => inner_start(d_init, z)
| (Right, Outer, _) => Zipper.move(d, z)
| (Right, Inner(_, c), (_, CanEnter(_, c_max))) when c == c_max =>
| (Right, Outer, _, Some(target_id)) => pass_fold(d, z, target_id)
| (Right, Outer, (_, CanEnter(d_init, _)), _) => inner_start(d_init, z)
| (Right, Outer, _, _) => Zipper.move(d, z)
| (Right, Inner(_, c), (_, CanEnter(_, c_max)), _) when c == c_max =>
pop_move(d, z)
| (Right, Inner(_), _) when chunkiness == ByToken => pop_move(d, z)
| (Right, Inner(delim, c), _) => inner_incr(delim, c, z)
| (Right, Inner(_), _, _) when chunkiness == ByToken => pop_move(d, z)
| (Right, Inner(delim, c), _, _) => inner_incr(delim, c, z)
};
};

Expand Down Expand Up @@ -219,11 +254,11 @@ module Make = (M: Editor.Meta.S) => {
/* Do move_action until the indicated piece is such that piece_p is true,
restarting from the beginning/end if not found in forward direction.
If no such piece is found, don't move. */
let do_until_wrap = (p, d, z) =>
switch (do_until(primary(ByToken, d), p, z)) {
let do_until_wrap = (p, d, z, ~folded) =>
switch (do_until(primary(ByToken, d, ~folded), p, z)) {
| None =>
let* z = to_edge(Direction.toggle(d), z);
do_until(primary(ByToken, d), p, z);
do_until(primary(ByToken, d, ~folded), p, z);
| Some(z) => Some(z)
};

Expand Down Expand Up @@ -316,19 +351,19 @@ module Make = (M: Editor.Meta.S) => {
};
};

let go = (d: Action.move, z: Zipper.t): option(Zipper.t) =>
let go = (d: Action.move, z: Zipper.t, ~folded): option(Zipper.t) =>
switch (d) {
| Goal(Piece(p, d)) => do_until_wrap(p, d, z)
| Goal(Piece(p, d)) => do_until_wrap(p, d, z, ~folded)
| Goal(Point(goal)) =>
let z = Zipper.unselect(z);
do_towards(primary(ByChar), goal, z);
do_towards(primary(ByChar, ~folded), goal, z);
| Extreme(d) => do_extreme(primary(ByToken), d, z)
| Local(d) =>
z
|> (
switch (d) {
| Left(chunk) => primary(chunk, Left)
| Right(chunk) => primary(chunk, Right)
| Left(chunk) => primary(chunk, Left, ~folded)
| Right(chunk) => primary(chunk, Right, ~folded)
| Up => vertical(Left)
| Down => vertical(Right)
}
Expand Down
17 changes: 15 additions & 2 deletions src/haz3lcore/zipper/action/Perform.re
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ let is_write_action = (a: Action.t) => {
switch (a) {
| Move(_)
| MoveToNextHole(_)
| Fold(_)
| Unfold(_)
| Unselect
| Jump(_)
| Select(_) => false
Expand All @@ -29,15 +31,26 @@ let go_z =
module Move = Move.Make(M);
module Select = Select.Make(M);
switch (a) {
| Fold(tid)
| Unfold(tid) =>
switch (Measured.find_by_id(tid, meta.measured)) {
| Some({origin, _}) =>
switch (Move.go(Goal(Point(origin)), z, ~folded=meta.folded)) {
| Some(z) => Ok(z)
| None => Ok(z)
}
| None => Error(Action.Failure.Cant_move)
}
| Move(d) =>
Move.go(d, z) |> Result.of_option(~error=Action.Failure.Cant_move)
Move.go(d, z, ~folded=meta.folded)
|> Result.of_option(~error=Action.Failure.Cant_move)
| MoveToNextHole(d) =>
let p: Piece.t => bool = (
fun
| Grout(_) => true
| _ => false
);
Move.go(Goal(Piece(p, d)), z)
Move.go(Goal(Piece(p, d)), z, ~folded=meta.folded)
|> Result.of_option(~error=Action.Failure.Cant_move);
| Jump(jump_target) =>
open OptUtil.Syntax;
Expand Down
2 changes: 2 additions & 0 deletions src/haz3lweb/Editors.re
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,8 @@ let put_editor = (ed: Editor.t, eds: t): t =>
};

let get_zipper = (editors: t): Zipper.t => get_editor(editors).state.zipper;
let get_folded = (editors: t): list(Id.t) =>
get_editor(editors).state.meta.folded;

/* Each mode (e.g. Scratch, School) requires
elaborating on some number of expressions
Expand Down
Loading
Loading