aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofBlockDelimiter.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-05-23 11:11:30 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-06 05:48:44 -0400
commit5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (patch)
treec803222d842bd96f3a25852633288e3aab14f45f /stm/proofBlockDelimiter.ml
parent07115d044cb97bc6c0a7323783d4d53e083d3e89 (diff)
STM: proof block detection/error resilience API
This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
0 files changed, 0 insertions, 0 deletions