Skip to content

Commit

Permalink
distinct tab presses for completing a token and move beyond it to nex…
Browse files Browse the repository at this point in the history
…t obligation
  • Loading branch information
dm0n3y committed Nov 8, 2024
1 parent a37d6a8 commit 026b44e
Showing 1 changed file with 10 additions and 11 deletions.
21 changes: 10 additions & 11 deletions src/core/editor/Move.re
Original file line number Diff line number Diff line change
Expand Up @@ -100,33 +100,32 @@ let complete_face = (site: Zipper.Site.t, ctx: Ctx.t) =>
switch (site) {
| Within(tok) =>
Token.complete(tok)
|> Option.map(tok =>
ctx |> Ctx.push(~onto=L, tok) |> Ctx.push(~onto=R, tok)
)
|> Option.value(~default=ctx)
|> Option.map(tok => ctx |> Ctx.push(~onto=L, Token.clear_marks(tok)))
| Between =>
open Options.Syntax;
let complete = side => {
let (face, ctx) = Ctx.pull(~from=side, ctx);
let* tok = Delim.to_opt(face);
let+ tok = Token.complete(tok);
Ctx.push(~onto=side, tok, ctx);
Ctx.push(~onto=L, tok, ctx);
};
// assuming this is only called when tabbing forward
let- () = complete(L);
let- () = complete(R);
ctx;
let/ () = complete(L);
complete(R);
};

let hole = (d: Dir.t, z: Zipper.t): option(Zipper.t) => {
switch (Zipper.cursor_site(z)) {
| (Select(_), _) => hstep(d, z)
| (Point(site), ctx) =>
let z =
open Options.Syntax;
// first try completing a face
let/ () =
switch (d) {
| L => z
| R => Zipper.mk(complete_face(site, ctx))
| L => None
| R => Option.map(Zipper.mk, complete_face(site, ctx))
};
// otherwise jump to next obligation
let c = Zipper.zip(~save_cursor=true, z);
let normal = Zipper.normalize(~cell=c);
let car =
Expand Down

0 comments on commit 026b44e

Please sign in to comment.