from a file position (range), find all syntax nodes inside

Stream: lean4

[Alissa Tung]

I am curious about, for a given file, give a file position (ln, col) or range (from_ln, from_col) ~ (end_ln, end_col), how can I find all syntax nodes inside it? If Lean server already can do the task, I am curious about where it is implemented.

[Marc Huisinga]

How it works right now, roughly:

• Lean.Language.mkIncrementalProcessor with Lean.Language.Lean.process and Lean.Server.FileWorker.setupImports gives us a language processor
• We run the language processor using a Lean.Parser.InputContext to obtain a Lean.Language.Lean.InitialSnapshot, representing a tree of asynchronous snapshots for the document
• The InitialSnapshot is converted to an IO.AsyncList using Lean.Server.FileWorker.mkCmdSnaps to obtain a list representation of the (still asynchronous) command snapshots
• When computing the response for a language server request, we run IO.AsyncList.waitFind? with a predicate like ·.endPos >= positionToFindCommandSnapshotAt to find the right snapshot
• Afterwards, we compute the response using the data in the snapshot (e.g. the Syntax of the command or its InfoTree) and functions like Lean.Syntax.findStack?; see Lean/Server/FileWorker/RequestHandling.lean for some examples

[Kim Morrison]

@Alissa Tung, in what sort of context are you hoping to run such a query?

[Alissa Tung]

Marc Huisinga 发言道：

How it works right now, roughly:

• Lean.Language.mkIncrementalProcessor with Lean.Language.Lean.process and Lean.Server.FileWorker.setupImports gives us a language processor
• We run the language processor using a Lean.Parser.InputContext to obtain a Lean.Language.Lean.InitialSnapshot, representing a tree of asynchronous snapshots for the document
• The InitialSnapshot is converted to an IO.AsyncList using Lean.Server.FileWorker.mkCmdSnaps to obtain a list representation of the (still asynchronous) command snapshots
• When computing the response for a language server request, we run IO.AsyncList.waitFind? with a predicate like ·.endPos >= positionToFindCommandSnapshotAt to find the right snapshot
• Afterwards, we compute the response using the data in the snapshot (e.g. the Syntax of the command or its InfoTree) and functions like Lean.Syntax.findStack?; see Lean/Server/FileWorker/RequestHandling.lean for some examples

Thank you, the explanation on this pipeline is very useful!