racket / drracket

DrRacket, IDE for Racket
http://www.racket-lang.org/
Other
445 stars 93 forks source link

New approach to lexing and indent? #521

Closed greghendershott closed 2 years ago

greghendershott commented 2 years ago

So I just noticed commit 73471198 adding drracket:range-indentation in addition to the existing drracket:indentation.

If I understand the motivation it's like Emacs letting a mode supply an indent-line and/or indent-region --- the latter may be faster or more correct than simply calling the former many times.

So that's good.

However both assume DrRacket -- or at least assume another tool is fine with a dependency on framework and gui-lib, and fine with the performance doing these things inter-process, and fine with some status quo weirdness about lexers.

Assumption/TL;DR

Most indenters rely on classification and "navigation".

Status quo

Classification and navigation are provided by color-lexer<%> and text<%>.

Goals

Indent needs a stream of tokens.

Sketch of proposal

So how about something like:


I realize this is a bit hand-wavy. It's based off a 1 year old lang-lexer branch of Racket Mode that I got working mostly satisfactorily (including experimental hacks to make the existing lexers behave as desired), but never merged. If you have deep or detailed questions, I'd need to reload my brain. But I wanted to float the general idea, at least, for now.

p.s. "Related work":

mflatt commented 2 years ago

Some of this has done to support the new expeditor replacement for readline, which uses the same indenting and navigation functions as DrRacket (via info) and doesn't use the editor or GUI libraries. But it's not currently done quite as you suggest.

On text%: expeditor supplies an indentation or navigation function with an object that provides some of the same methods as text%. I imagined pinning down that interface and providing it as a separate library, and then declaring that indentation and navigation functions are supposed to stay within that interface instead of expecting a full color:text%. I think that library would play the role that you're calling token-map.

On parentheses: a language info can currently provide drracket:paren-matches in addition to color-lexer. It's too bad those pieces aren't together, since they need to work together, but at least parentheses can be specified currently.

greghendershott commented 2 years ago

Thanks for the reply.

On parentheses: a language info can currently provide drracket:paren-matches in addition to color-lexer. It's too bad those pieces aren't together, since they need to work together, but at least parentheses can be specified currently.

Aha, I see that now, as of commit 046a0c9.

On text%: expeditor supplies an indentation or navigation function with an object that provides some of the same methods as text%. I imagined pinning down that interface and providing it as a separate library, and then declaring that indentation and navigation functions are supposed to stay within that interface instead of expecting a full color:text%. I think that library would play the role that you're calling token-map.

OK I'll take a look at that.

greghendershott commented 2 years ago

Although I don't grok all the code yet:

It's a revelation to see how how simple the definition of like-text% is -- how small a subset of text% methods could be needed by an indenter. That's great.

For my purposes I believe I need a variant of like-text% that includes an update method, along the lines of this from my year-old branch. What I had done then was have Emacs buffer-change notifications update the tokens --- effectively update the token map after every user keystroke or edit. (Because if they press ENTER you need it for indent immediately anyway, and lazy is trickier than just making it fast enough if possible.)

Caveats:

So: I'm not sure where such a thing should live:

Depending on what you think, I could open an issue on expeditor instead, or none (just pursue it solo). And in any case close this issue, here.

mflatt commented 2 years ago

A new package sounds right, and if you have time and interest to work on it, that's fantastic. In that case, I'll be happy to update expeditor to use your library when it's ready — and for the docs on "info.rkt"-based tools to eventually refer to that package as defining the available interface. A dependency on data-lib seems entirely reasonable.

Your constraint on update that tokenization converges "soon" sounds right. Assuming I understand, DrRacket similarly has to wait on tokenization for indentation support, and expeditor would be improved by having update available instead of just re-lexing every time.

rfindler commented 2 years ago

I am also in 100% agreement that you looking into this is fantastic!

I think your status quo description is right.

Right now the way that DrRacket achieve this bullet:

It supplies efficient (update! tm pos old-len str) re-tokenizing (fast enough to be called during user typing/editing).

is by doing only some of the work (most of the time it does only some of the work) and using the GUI event queue to postpone some work so the eventqueue can handle user input. Assuming that you're sticking with the current tokenizer interface to determine the colors, then I am not sure that we can really do better than that. That is, under the constraint that we stick with the tokenizer interface I don't think it can return fast enough to be interactive and still always have the buffer be completely correctly colored (as opposed to pausing to handle events while the buffer is known to be partly wrong).

The reason there's this tight integration between the colorer and the GUI eventloop is also because updating the colors of a specific region (so that the user sees them) needs to be done on the eventloop thread, not just in some other space, in order to interoperate with text%.

Were you thinking of replacing the colorer in DrRacket? I'd be in favor of that, partly because we need two implementations of this like we need an extra hole in our heads and partly because the existing implementation is one of the places where DrRacket feels slow (watching the colors march down the 20,000 overview). If so, there would probably needs to be some callbacks callouts from the data structure you have to tell the UI that colors need to change in the editor? Am I understanding things properly?

Another question: there's also the VS Code/language server integration: would the APIs you have in mind work with them too? Is that in scope for what you have in mind?

greghendershott commented 2 years ago

@mflatt Modulo any unknown (to me) unknowns, I already did most of the work a year ago. Over the next month or two (say) I think I have time to:

greghendershott commented 2 years ago

@rfindler The token-map I had designed basically wraps an interval-map of half-open position intervals to lexer results.

To let update avoid re-lexing from the start, it also has an interval-map of lexers used for various positions.

To let update avoid re-lexing all the way to the end: I have it assume that, if it eventually starts getting exactly the same tokens as before -- albeit with the positions merely shifted by exactly the length of the inserted/removed text that prompted the update -- it has "converged" and we would keep getting that all the way to the end. So we can just stop early; use a fast interval-map shift op on the positions of the remainder.

Anyway, update returns a list of the positions/tokens that it discovered actually did change; e.g. a list of (from upto token) tuples. The caller can use those values to update whatever kind of UI it needs to.

I think none of that dictates how/when you call update and use the list of changed tokens to update the UI. I don't think it would force Dr Racket to work differently/slower. But would it allow Dr Racket to work faster? I think it might because the re-tokenizing per se (update) is fast enough that you might no longer need to delay UI updating for that reason. (I'm not sure about other reasons you need to delay?)

So for example I think you could get an input character event, call update (yes, for every single char, really!), and update text<%> or however that works to refresh the UI --- all on the eventloop thread.

[You can of course delay calling update, but you'd need to force it before you indent (as soon as the user hits enter or tab or whatever) because indent (generally) needs classification and expr nav. So I found in practice (with Emacs on the front end) trying to be lazy doesn't give much benefit, and gets into the usual trickiness of coordinating laziness and forcing. So on balance I found it better to "just" make update "fast enough".]


Were you thinking of replacing the colorer in DrRacket? I'd be in favor of that, partly because we need two implementations of this like we need an extra hole in our heads and partly because the existing implementation is one of the places where DrRacket feels slow (watching the colors march down the 20,000 overview). If so, there would probably needs to be some callbacks callouts from the data structure you have to tell the UI that colors need to change in the editor? Am I understanding things properly?

Yes I imagined that would be possible. Although I doubt I'll have time to lead/do that work myself, I'd be happy to help you or someone else work on that, and also adapt things to make that easier/faster/better.

Another question: there's also the VS Code/language server integration: would the APIs you have in mind work with them too? Is that in scope for what you have in mind?

Yes, I think it's in scope.

The token-map "API" is small/narrow. It expects it might need to live in some "back end" process that will be talking to another "front end" via some serialization like s-expressions or json, not Racket values.

Last I looked, at least one of the vscode/LSP solutions for Racket was already using syntax-color; the missing piece was indent. That may have changed. Anyway if they still have a to-do I'm happy to coordinate.

Same for vim, or someone who wants to use any of this in some other, non-editor kind of tool.

mflatt commented 2 years ago

One thought on indentation: the default Racket indenter may need to move so that it can be used outside of the framework.

Currently, expeditor has its own Racket indenter, just because that was mostly there in the starting code from Chez Scheme. It doesn't know about Racket indentation preferences, and it probably behaves differently in other ways. That didn't seem like a big deal when going from zero command-line indentaton support to some support, but obviously isn't best.

Metaxal commented 2 years ago

On a side note, such an indenter could also be used by @sorawee 's fmt, and would help ensure consistency of indentation rules across tools.

rfindler commented 2 years ago

I don't think it would force Dr Racket to work differently/slower. But would it allow Dr Racket to work faster? I think it might because the re-tokenizing per se (update) is fast enough that you might no longer need to delay UI updating for that reason. (I'm not sure about other reasons you need to delay?)

This sounds great!

A test case I use sometimes is to open drracket/private/unit and then insert a open double quote somewhere near the beginning. This forces relexing of the entire buffer. Does this finish in <= 20 msec or so?

sorawee commented 2 years ago

@Metaxal fmt would not use the indenter, but it does use the tokenizer, so this discussion is relevant to the work. Thanks for mentioning!

@greghendershott

The status quo lexer handling can be inconsistent or at least confusing: delimit is one of the chars ()[]{}, and, it simply "restates" information from the lexeme I think the justification for this is that e.g. racket-lexer handles #( as a single 2-char token, parenthesis (. [However it handles #'( as two tokens --- a 2-char #' token constant followed by a 1-char parenthesis ( token. ??] In any case it's an impoverished notion of delimiters wrt all langs.

For #' vs #, I think the current behavior makes sense

#'
(1 2 3)

should lex successfully, but

#
(1 2 3)

does not necessarily to? (read would fail to read the latter code)


So far, in fmt, I use module-lexer to lex the whole content from scratch. I then "group" tokens together as a tree (primarily based on parens), so that each node is either visible or invisible (invisible ones would be either whitespaces, block comments, line comments, or S-exp comments -- including their "contents"). I'm not sure if there's any possible improvement on this front so that I do not need to perform this grouping manually.

The performance bottleneck in fmt is in the pretty printing algorithm, so I don't concern too much with lexing/grouping from scratch if that's necessary. Though if it's not too hard to switch to the "update" approach, I'd love to do that.

greghendershott commented 2 years ago

One thought on indentation: the default Racket indenter may need to move so that it can be used outside of the framework.

Yes, for sure. Just (get-info 'drracket:indentation) means blammo you've loaded all of framework. To avoid that, on my WIP branch I had gone ahead and made my own sexp and at-exp indenters, but that was just a WIP hack.


There's a whole other conversation about customizing indentation at granularity other than #lang.

  1. Not breaking Dr Racket user indentation preferences for sexp langs.
  2. Not breaking Emacs user indentation preferences for sexp langs (via putting a property on a symbol).
  3. Letting a macro definition specify its indentation somehow and conveying that somehow to tools.

I don't have great answers for those yet, but 1 and 2 at least should be addressed as "don't make things worse" even if 3 isn't yet.

rfindler commented 2 years ago

So far, in fmt, I use module-lexer to lex the whole content from scratch. I then "group" tokens together as a tree (primarily based on parens), so that each node is either visible or invisible (invisible ones would be either whitespaces, block comments, line comments, or S-exp comments -- including their "contents"). I'm not sure if there's any possible improvement on this front so that I do not need to perform this grouping manually.

I'm not sure it is really easy to reuse, but I believe that color:text is also doing this job.

rfindler commented 2 years ago

There's a whole other conversation about customizing indentation at granularity other than #lang.

  1. Not breaking Dr Racket user indentation preferences for sexp langs.

I'm comfortable moving away from this somehow. It would be nice to respect a user's preferences here somehow but perhaps it would only work when some preference is set (and setting that preference would use lots of old code instead of all this cool new code we're talking about).

greghendershott commented 2 years ago

@rfindler

A test case I use sometimes is to open drracket/private/unit and then insert a open double quote somewhere near the beginning. This forces relexing of the entire buffer. Does this finish in <= 20 msec or so?

Yes I love this file and class-internal.rkt because at 5000 lines they're 10X bigger than the style guide says. :smile: Seriously I use them for smoke testing. I even added the latter to the test suite for (status quo) indent and font-lock, recently.

  1. When I try the unmatched " near the start, with my WIP branch, update takes about 1300 msec CPU/real time. Not very good. What this tests: update detecting it actually needs to re-lex the entire file, and doing so.

  2. When I do other typing near the start, update is around 4-10 msec CPU/real time. Quite good, I think; doesn't feel sluggish to me when typing fast. What this tests: update detecting convergence and not actually needing to re-lex the entire file; just shift positions in the interval-map.

So I think the unmatched " is an important edge case but it's not exercising the ability of update to avoid unnecessary work?

My memory from a year ago is I noticed this and felt, "Well, 1 second isn't great, but it's not horrible, and if people use fancy things like paredit or even just boring old electric-pair-mode, they'll probably get balanced quotes in the first place, so... it needs attention but not the highest item on my list".

But I would look into it again, now. How much of the time is the re-lexing per se, vs. other work? Would a "streaming/batching" response help, hurt, or be N/A? Any other ideas? etc.

greghendershott commented 2 years ago

There's a whole other conversation about customizing indentation at granularity other than #lang.

  1. Not breaking Dr Racket user indentation preferences for sexp langs.

I'm comfortable moving away from this somehow. It would be nice to respect a user's preferences here somehow but perhaps it would only work when some preference is set (and setting that preference would use lots of old code instead of all this cool new code we're talking about).

I can't speak for all users, but my impression/experience is that people set custom indent in tools only because there is no mechanism to specify indent

In other words if people could do this at the language level, I think they would be OK -- or even delighted -- to stop doing it "externally" at the tool level.

rfindler commented 2 years ago

@greghendershott

So I think the unmatched " is an important edge case but it's not exercising the ability of update to avoid unnecessary work?

Yes, that sounds right to me.

This kind of potential badness is the reason why the the color:text stuff is incremental. It is cps'd to be able to pause, and it pauses only at a token boundary. That is, the assumption is that getting one single next token (via a call to a lexer) is always going to finish quickly. There's a loop that checks the time budget and sometimes lexes one more and sometimes just pauses itself. Then there is also an operation that says "I want to wait for the results to be done" and that gets used by keystrokes like "forward sexp" which then "block" until the coloring information is complete and the paren matching is sync'd up and then they can set the insertion point.

Here's some code that, I think, does the same experiment that you were doing. It is hard to say if this is an apples to apples comparison, but I think the first time result corresponds to processing the entire buffer (after inserting an open quote at the start of the second line (so just below the #lang line)). The second one is updating internal editor data structures to record the colors so that a refresh actually draws the right things so I think that's beyond what is happening in your test, but it is also much slower. So it might be doing some of what you're doing too, I'm not 100% sure.

#lang racket

(require framework)
(define t (new racket:text%))
(void (send t load-file (collection-file-path "unit.rkt" "drracket" "private")))
(send t freeze-colorer)
(send t thaw-colorer)
(collect-garbage) (collect-garbage) (collect-garbage)

;; this is lexing the buffer, using the `finish-now` method in color:text
(time
 (send t insert "\""
       (send t paragraph-start-position 1)
       (send t paragraph-start-position 1))
 (send t freeze-colorer))

;; I think this is actually updating the editor with the colors and so 
;; different from what the test you were running does.
(time (send t thaw-colorer))

The assumption that the lexer completes quickly might not always be true if there are, say, giant strings but we could tackle that by having more complex token interface that allowed a colorer to stop after some portion of a token and promise that there's more of the token to come. I have not tried any timing tests to see if this matters,tho.

greghendershott commented 2 years ago

Thanks I'll mull that over as well.

It may well be that in Dr Racket this should remain interruptible/resumable. After all, in Racket we have nice means for coordinating such things.

By contrast I found it trickier to do reliably/correctly via IPC between single-threaded Emacs front end process and the Racket mode back end -- e.g. try to be lazy, then force for an indent or nav. Early on that pushed me toward seeing if update could be fast enough to do eagerly and "ridiculously frequently".

But just because it's faster doesn't mean Dr Racket should use it eagerly.

Also although coordinating concurrency is harder for me, I just set Emacs properties on ranges in the buffer, and the rendering is not my job. So somewhat different concerns.


By the way, here's another test case: Insert #| near the start of unit.rkt.

Here for me the # is 20 msec and the | is another 30 msec. The whole 5,000 line file is "instantly" colored as a comment.

So the lexer flies through that and token-map returns that one (very long span) token very quickly.

So it seems proportional to the number of updated tokens. A lone " near the start of a long file, especially one with existing " string tokens, is an excellent way to produce many changed tokens.

(Which you probably already knew, I'm just writing out loud.)

samth commented 2 years ago

Just for fun, I tried some very large JS files (5000-100000 lines) in VS Code. Inserting a "`" character at the beginning (which creates a string literal) seems to happen almost instantly, but there's definitely incrementatlity in the coloring -- I think it just colors the portion shown on the screen first, and then the rest.

aowens-21 commented 2 years ago

@greghendershott

I can't speak for all users, but my impression/experience is that people set custom indent in tools only because there is no mechanism to specify indent

* in a syntax definition

* for an existing definition that neglected to specify it correctly or at all

In other words if people could do this at the language level, I think they would be OK -- or even delighted -- to stop doing it "externally" at the tool level.

I'm not sure if it's worth mentioning here, but this is roughly what @shhyou and I are trying accomplish with racket-formatting. It isn't exactly advertised because it's still more of a prototype than something we expect people to use all over the place, but it lets macro authors attach formatting rules to their macros using a DSL we've provided. Then on the IDE side, DrRacket (or racket-mode or presumably any Racket environment that wants to look for those formatting rules on the syntax objects could use them to format code). I haven't thought much about how it interacts with user preferences, but it could probably be configured to fall back to user preferences when a macro author hasn't added any formatting rules (which right now would be 99.9% of macros).

greghendershott commented 2 years ago

@samth That's also my experience with status quo racket-mode buffers in Emacs. Although I don't know about vscode, in Emacs the base level isn't even "tokens" it's character classification, with a special case pattern for two-character comment begin/end sequences. Although there's an optional "syntax propertize function" that can handle arbitrary things like say here docs, the basics for things like strings and comments are a lookup table in Emacs' C core.

Anything where a Racket Mode buffer needs to marshal edits from Emacs to another process that runs a Racket lexer, and responds with tokens, which end up as highlighting back in the buffer, is going to be... at least somewhat slower. When I experimented with this a year ago, I was pleasantly surprised that it wasn't completely awful. With some more work, it became overall mostly reasonable IMHO for "typical" cases. But it could use more improvement for sure. Probably streaming/batching the tokens response is part of the answer.


p.s. As a Racket Mode user, I am fine with the status quo wrt highlighting and indent. My personal needs are met. Taking something that works well, and making it work less-well, differently... is not usually how I prefer to spend my time. At all. :smile: But if Racket is supposed to be a programming-language programming language, and if that includes more non-sexp langs, and if good tooling is part of the whole P-LPL story, then the scope of "working well" is bigger.


p.p.s. As an Emacs user, where an approximate equivalent of #lang is "major mode", I would probably be fine something where a #lang generates Emacs Lisp code defining a major mode. (I am joking but only partly.) But I hear there are people who use neither Emacs nor Dr Racket, as hard as that may be to believe.

rfindler commented 2 years ago

Just for fun, I tried some very large JS files (5000-100000 lines) in VS Code. Inserting a "`" character at the beginning (which creates a string literal) seems to happen almost instantly, but there's definitely incrementatlity in the coloring -- I think it just colors the portion shown on the screen first, and then the rest.

I think DrRacket will feel interactive in a similar situation but the actual coloring itself will be slower. (You can see things progress down the program contour but the visible part of the buffer changes pretty much instantly.) My current belief is that the editor's data structures (not the colorer per se) are what would need to be improved. There is also a lingering suspicion that the actually calls to draw text that draw the characters on the screen are slow, but @mflatt put a lot of effort into that and I'm not sure we can do better there.

rfindler commented 2 years ago

@greghendershott writes,

It may well be that in Dr Racket this should remain interruptible/resumable. After all, in Racket we have nice means for coordinating such things.

By contrast I found it trickier to do reliably/correctly via IPC between single-threaded Emacs front end process and the Racket mode back end -- e.g. try to be lazy, then force for an indent or nav. Early on that pushed me toward seeing if update could be fast enough to do eagerly and "ridiculously frequently".

But just because it's faster doesn't mean Dr Racket should use it eagerly.

Also although coordinating concurrency is harder for me, I just set Emacs properties on ranges in the buffer, and the rendering is not my job. So somewhat different concerns.

If I did the experiment right, I'm seeing 266 msec for the "insert an open quote after the hash lang line" test case using your code, which isn't fast enough to block the event-handling thread, I would say. But I do 100% agree that the architecture is different enough that different solutions seem appropriate here. If I am understanding your setup correctly, when the edit comes in, you send a message off to the racket process and you don't block on the reply before handling other edits. Then, when a reply is ready, it'll come back and you can recolor the buffer. Is that right? So the actual state of the buffer is (morally) in two places: there is a copy of the buffer's content on the racket side as well as one down inside Emacs somewhere? In the racket setup, there's just one, and edits are happening "together" (the user typing something calls the text% method insert and the colorer changing the colors calls the text% method change-style). I'm not sure where to go with this observation, just trying to get my head around the situation(s)! :)


By the way, here's another test case: Insert #| near the start of unit.rkt. Here for me the # is 20 msec and the | is another 30 msec. The whole 5,000 line file is "instantly" colored as a comment.

I see something similar, but slower. I see 138msec for the first call to time in the example code I sent earlier (that uses racket:text stuff) and then 2 msec for the second call to time (the one that updates the text% data structures). I also see that just calling the racket-lexer directly on a port with a string that has #| followed by the entire content of "unit.rkt" takes 14 msec so something is fishy with that 138 msec. Maybe there are some improvements I can make somewhere.


Here's the code I wrote that is doing the "insert an open quote at the start" with @greghendershott 's code; just posted here in case I'm doing something dumb that is messing up the timings I'm reporting!

#lang racket
(require "core.rkt")

(define test-file
  (collection-file-path "unit.rkt" "drracket" "private"))

(define insertion-point
  (call-with-input-file test-file
    (λ (port)
      (port-count-lines! port)
      (read-line port)
      (define-values (line col pos) (port-next-location port))
      pos)))

(define tm
  (call-with-input-file test-file
    (λ (port)
      (define sp (open-output-string))
      (copy-port port sp)
      (create (get-output-string sp)))))

(time (void (update! tm insertion-point 0 "\"")))
greghendershott commented 2 years ago

I'll explore more ideas about performance. I'll just need some time to reload my brain with various ideas and details from a year ago.

Meanwhile, just a couple other points:

rfindler commented 2 years ago

I'll explore more ideas about performance. I'll just need some time to reload my brain with various ideas and details from a year ago.

Thank you!

Meanwhile, just a couple other points:

* Another edge case: Someone adds that `"` near the start of `unit.rkt`, selects the whole buffer, does a Cut, then a Paste. The entire buffer will change, _and_ the cursor is at the _end_. AFAICT the entire buffer must be re-lexed before anything can be colored or indented near the end of it. I think _this_ is one edge case that's just unavoidably slow? But understandably/tolerably?

I'm not sure if I'm getting this point correctly, so apologies if this doesn't make sense :) but the way the colorer in the framework does this is that it just knows that some region has the wrong colors and, when it gets there, it fixes that part. Although, to be clear, insertion and deletion slides stuff over, colors and all, and this happens at a lower layer, directly in the editor. (Of course those colors might be wrong but just sliding things along is a good thing to do cheaply.)

So if someone were to cut and paste the entire buffer, that looks a lot like opening the file from scratch, so the stuff at the bottom will remain black and white for quite a while. In DrRacket if you use the "View|Show Program Contour" menu item, you'll see something where you can watch the colors march down the screen.

* This is getting somewhat off-topic, but: So far we're talking about indent, which only needs lexical tokens, and "lexical highlighting", which (by definition) needs only lexical tokens. Another interesting thing is what some people call "semantic highlighting". For instance, an identifier at a definition site (e.g. `define` or `let`) might have a distinct appearance. Of course this shades off into what check-syntax does, which has its own update and performance characteristics. Anyway, you could imagine an initial/quick lexical highlighting, that after some delay is partially overwritten/enhanced by semantic highlighting if/when that information becomes available. [Status quo: Racket Mode is already more colorful/baroque/garish, depending on your opinion. But it does this with dumb/static rules for certain known forms like `define` in `#lang racket`. The WIP hash-lang-mode using the lang lexer is more "plain", just like Dr Racket. I could imagine it becoming less-plain again, someday, but via actual semantic highlighting that would work for any lang.]

I think it would be great to get more of what Racket mode is doing in DrRacket along these lines. And even better if we can share the code that figures it all out!

greghendershott commented 2 years ago

In that scenario I'm mainly thinking of indent.

Anything that needs lexed tokens to proceed, needs to wait for them to be available before it can proceed.

In the whole-huge-file-changed, cursor-at-end scenario:

That's why I believe that scenario is unavoidably "hopeless".

AFAICT indent forces any delay; it's a hard synchronization point. All you can do is hope for a minimal amount of work needed to proceed.

rfindler commented 2 years ago

@greghendershott I agree with all of that! What you describe is what's currently happening in DrRacket, in fact. (You can see this scenario by doing meta-> on unit.rkt for example.)