Incremental processing of files

Stream: lean4

[Auguste Poiroux]

Hi!
I am interested in processing Lean files incrementally, similar to what is happening in VS Code with the Lean 4 extension. I have been playing around with IO.processCommandsIncrementally but it seems that it only processes full commands one after the other, i.e. one declaration + implementation/proof at a time. I should have guessed given the name ^^
However, this doesn't exactly mirror what is happening in VS Code as tactics seem to be processed incrementally as well. Do you know the name of the incremental method behind the Lean 4 extension file processing?
Thanks!

[Auguste Poiroux]

After having a look into the Lean 4 LSP, it seems that my question was a bit naive. I am not sure I can get something similar to IO.processCommandsIncrementally but more fine-grained and getting a list of IncrementalState.
But now I am a bit curious: why does IO.processCommandsIncrementally exist?