lean4-htt/src/Init/System
Sebastian Ullrich 6b0e7e1f46
feat: synchronous execution of task continuations (#3013)
In the new snapshot design, we have a tree of `Task`s that represents
the asynchronously processed document structure. When transforming this
tree in response to a user edit, we want to quickly run through
reusable, already computed nodes of the tree synchronously and then
spawn new tasks for the new parts. The new flag allows us to do such
mixed sync/async tree transformations uniformly. This flag exists as
e.g.
[`ExecuteSynchronously`](https://learn.microsoft.com/en-us/dotnet/api/system.threading.tasks.taskcontinuationoptions?view=net-8.0)
in other runtimes.
2024-01-25 13:54:20 +00:00
..
FilePath.lean fix: do not strip dotted components from lean module names (#2994) 2024-01-10 14:24:26 +00:00
IO.lean feat: synchronous execution of task continuations (#3013) 2024-01-25 13:54:20 +00:00
IOError.lean feat: log2 for Fin and UInts 2022-11-29 01:05:06 +01:00
Mutex.lean chore: use deriving Nonempty 2022-12-22 03:48:15 +01:00
Platform.lean feat: System.Platform.target (#3207) 2024-01-24 12:11:00 +00:00
Promise.lean chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
ST.lean feat: code action resolvers 2022-10-20 11:20:42 -07:00
Uri.lean chore: fix more typos in comments 2023-10-08 14:37:34 -07:00