aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vcs.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-05-11 14:53:46 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-06 05:48:44 -0400
commit17f3346c5c42c16eed58bf2325aa996c3892a5e9 (patch)
tree632e37cb16782f02fe33ef51d88ff04952a8dd9a /stm/vcs.mli
parentc4789644ab4d1a88f1331efb29b69011a30f5eed (diff)
STM: invalid states are first class citizens
A state in the cache (document node) is now one of "Empty | Error | Valid". This paves the way to commands/blocks-of-commands resilient-to/confining errors: one can catch and "ignore" the exception obtained by reaching the previous state and do something sensible, like running anyway the command or skipping until the end of an error-confining block is reached. Invalid states carry an enriched exception with the safe_id attached, so that if one edits_at or observe them gets a safe place to land (CoqIDE needs such piece of info). Little API change in Stm.state_of_id now returning a `Error variant for the new kind of state.
Diffstat (limited to 'stm/vcs.mli')
0 files changed, 0 insertions, 0 deletions