refactor(library/task_queue): extract library-specific code

src/library/CMakeLists.txt

@@ -16,5 +16,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
   aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
   locals.cpp normalize.cpp discr_tree.cpp
-  task_queue.cpp mt_task_queue.cpp st_task_queue.cpp
+  task_queue.cpp mt_task_queue.cpp st_task_queue.cpp task_helper.cpp
   messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp)

src/library/mt_task_queue.cpp

@@ -10,6 +10,7 @@ Author: Gabriel Ebner
 #include "library/mt_task_queue.h"
 #include "util/interrupt.h"
 #include "util/flet.h"
+#include "task_helper.h"
 
 #if defined(LEAN_MULTI_THREAD)
 namespace lean {
@@ -105,7 +106,7 @@ void mt_task_queue::spawn_worker() {
                 scoped_current_task scope_cur_task(&t);
                 lock.unlock();
                 if (cb) cb(t->m_task);
-                is_ok = t->execute();
+                is_ok = execute_task_with_scopes(&*t);
                 lock.lock();
             }
             reset_interrupt();

src/library/st_task_queue.cpp

@@ -6,6 +6,7 @@ Author: Gabriel Ebner
 */
 #include <vector>
 #include "library/st_task_queue.h"
+#include "task_helper.h"
 
 namespace lean {
 
@@ -44,7 +45,7 @@ void st_task_queue::submit(generic_task_result const & t) {
     }
 
     if (m_progress_cb) m_progress_cb(t->m_task);
-    bool is_ok = t->execute();
+    bool is_ok = execute_task_with_scopes(&*t);
     t->m_state = is_ok ? task_result_state::FINISHED : task_result_state::FAILED;
     t->clear_task();
 }

src/library/task_helper.cpp

@@ -0,0 +1,44 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#include <string>
+#include <library/trace.h>
+#include <library/message_builder.h>
+#include "library/task_helper.h"
+
+namespace lean {
+
+bool execute_task_with_scopes(generic_task_result_cell * task) {
+    lean_assert(!task->has_evaluated());
+    try {
+        scoped_task_context ctx(task->m_task->get_module_id(), task->m_task->get_task_pos());
+        scope_message_context scope_msg_ctx(task->m_task->get_bucket());
+        try {
+            scope_traces_as_messages scope_traces(task->m_task->get_module_id(), task->m_task->get_pos());
+            task->execute_and_store_result();
+        } catch (task_cancellation_exception) {
+            throw;
+        } catch (interrupted) {
+            throw;
+        } catch (throwable & ex) {
+            environment env;
+            message_builder builder(env, get_global_ios(), task->m_task->get_module_id(), task->m_task->get_pos(), ERROR);
+            builder.set_exception(ex);
+            builder.report();
+            throw;
+        }
+        return true;
+    } catch (interrupted) {
+        task->m_ex = std::make_exception_ptr(
+                task_cancellation_exception(generic_task_result(task)));
+        return false;
+    } catch (...) {
+        task->m_ex = std::current_exception();
+        return false;
+    }
+}
+
+}

src/library/task_helper.h

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#pragma once
+#include "library/task_queue.h"
+
+namespace lean {
+
+bool execute_task_with_scopes(generic_task_result_cell * task);
+
+}

src/library/task_queue.cpp

@@ -5,8 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 */
 #include <string>
-#include <library/trace.h>
-#include <library/message_builder.h>
 #include "library/task_queue.h"
 
 namespace lean {
@@ -30,36 +28,6 @@ void generic_task_result_cell::clear_task() {
     }
 }
 
-bool generic_task_result_cell::execute() {
-    lean_assert(!has_evaluated());
-    try {
-        scoped_task_context ctx(m_task->get_module_id(), m_task->get_task_pos());
-        scope_message_context scope_msg_ctx(m_task->get_bucket());
-        try {
-            scope_traces_as_messages scope_traces(m_task->get_module_id(), m_task->get_pos());
-            execute_and_store_result();
-        } catch (task_cancellation_exception) {
-            throw;
-        } catch (interrupted) {
-            throw;
-        } catch (throwable & ex) {
-            environment env;
-            message_builder builder(env, get_global_ios(), m_task->get_module_id(), m_task->get_pos(), ERROR);
-            builder.set_exception(ex);
-            builder.report();
-            throw;
-        }
-        return true;
-    } catch (interrupted) {
-        m_ex = std::make_exception_ptr(
-                task_cancellation_exception(generic_task_result(this)));
-        return false;
-    } catch (...) {
-        m_ex = std::current_exception();
-        return false;
-    }
-}
-
 LEAN_THREAD_PTR(task_queue, g_tq);
 scope_global_task_queue::scope_global_task_queue(task_queue * tq) {
     m_old_tq = g_tq;

src/library/task_queue.h

@@ -24,7 +24,7 @@ enum class task_result_state {
 };
 
 class generic_task;
-class generic_task_result_cell {
+struct generic_task_result_cell {
     MK_LEAN_RC()
     void dealloc() { delete this; }
 
@@ -51,7 +51,6 @@ class generic_task_result_cell {
     }
 
     virtual void execute_and_store_result() = 0;
-    bool execute();
 };
 
 class generic_task_result {