From b6e79d646de16da4cada0be3f566aa18b6a656ea Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 1 Mar 2017 18:31:22 +0100 Subject: [PATCH] fix(util/cancellable): actually set interrupt flag --- src/util/cancellable.cpp | 5 ++++- src/util/cancellable.h | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/util/cancellable.cpp b/src/util/cancellable.cpp index e345f9932c..f3294e5797 100644 --- a/src/util/cancellable.cpp +++ b/src/util/cancellable.cpp @@ -49,7 +49,10 @@ cancellation_token mk_cancellation_token(cancellation_token const & parent) { LEAN_THREAD_PTR(cancellation_token const, g_cancellation_token); scope_cancellation_token::scope_cancellation_token(cancellation_token const * tok) : - flet(g_cancellation_token, tok) {} + flet(g_cancellation_token, tok), + scoped_interrupt_flag(*tok ? (*tok)->get_cancellation_flag() : nullptr) { + check_interrupted(); +} cancellation_token global_cancellation_token() { return g_cancellation_token ? *g_cancellation_token : nullptr; diff --git a/src/util/cancellable.h b/src/util/cancellable.h index 617829691c..6319f525e0 100644 --- a/src/util/cancellable.h +++ b/src/util/cancellable.h @@ -9,6 +9,7 @@ Author: Gabriel Ebner #include #include "util/thread.h" #include "util/flet.h" +#include "interrupt.h" namespace lean { @@ -36,6 +37,8 @@ public: void gc(); void cancel(std::shared_ptr const & self) override; + + atomic_bool * get_cancellation_flag() { return &m_cancelled; } }; cancellation_token mk_cancellation_token(cancellation_token const & parent); @@ -44,7 +47,7 @@ inline cancellation_token mk_cancellation_token() { return mk_cancellation_token inline void cancel(std::shared_ptr const & c) { if (c) c->cancel(c); } inline void cancelw(std::weak_ptr const & wc) { if (auto c = wc.lock()) cancel(c); } -struct scope_cancellation_token : flet { +struct scope_cancellation_token : flet, scoped_interrupt_flag { scope_cancellation_token(cancellation_token const *); scope_cancellation_token(cancellation_token & t) : scope_cancellation_token(&t) {} };