From 026b44e301d7d73b426704377153582a6440fd58 Mon Sep 17 00:00:00 2001 From: David Moon Date: Fri, 8 Nov 2024 10:59:45 -0500 Subject: [PATCH] distinct tab presses for completing a token and move beyond it to next obligation --- src/core/editor/Move.re | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/core/editor/Move.re b/src/core/editor/Move.re index d5d2f793..e3965369 100644 --- a/src/core/editor/Move.re +++ b/src/core/editor/Move.re @@ -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 =