From 17f3346c5c42c16eed58bf2325aa996c3892a5e9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 May 2016 14:53:46 +0200 Subject: 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. --- stm/stm.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index 6ffe0beb4..d825ff33e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -122,7 +122,7 @@ type state = { proof : Proof_global.state; shallow : bool } -val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] +val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] (** read-eval-print loop compatible interface ****************************** **) -- cgit v1.2.3