From 45820531c43de0ebc1ebaa2efbc4398e27de0a10 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 24 Feb 2017 15:21:59 +0100
Subject: [PATCH] refactor(util/task): remove switch to disable priority
 inversion

---
 src/library/mt_task_queue.cpp | 3 +--
 src/util/task.h               | 1 -
 src/util/task_builder.h       | 6 ------
 3 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/src/library/mt_task_queue.cpp b/src/library/mt_task_queue.cpp
index 0453076af3..23930ff95b 100644
--- a/src/library/mt_task_queue.cpp
+++ b/src/library/mt_task_queue.cpp
@@ -215,12 +215,11 @@ bool mt_task_queue::check_deps(gtask const & t) {
         get_data(t)->m_imp->get_dependencies(deps);
     } catch (...) {}
 
-    auto do_prio_inv = get_data(t)->m_flags.m_do_priority_inversion;
     auto prio = get_prio(t);
     for (auto & dep : deps) {
         if (dep) {
             submit_core(dep, prio);
-            if (do_prio_inv) bump_prio(dep, prio);
+            bump_prio(dep, prio);
         }
     }
 
diff --git a/src/util/task.h b/src/util/task.h
index 5d1e4cca91..67472d773f 100644
--- a/src/util/task.h
+++ b/src/util/task.h
@@ -24,7 +24,6 @@ struct scheduling_info {
 };
 
 struct task_flags {
-    bool m_do_priority_inversion = true;
     bool m_needs_separate_thread = true;
     bool m_eager_execution = false;
 };
diff --git a/src/util/task_builder.h b/src/util/task_builder.h
index 56a75f59e4..50c15d84cf 100644
--- a/src/util/task_builder.h
+++ b/src/util/task_builder.h
@@ -68,12 +68,6 @@ public:
             m_imp(new base_task_imp<Fn>(std::forward<Fn>(fn))),
             m_cancel_tok(global_cancellation_token()) {}
 
-    task_builder<Res> disable_priority_inversion() {
-        lean_assert(m_imp);
-        m_flags.m_do_priority_inversion = false;
-        return std::move(*this);
-    }
-
     task_builder<Res> does_not_require_own_thread() {
         lean_assert(m_imp);
         m_flags.m_needs_separate_thread = false;