refactor(library/message_buffer): extract definitions into extra header file

src/kernel/pos_info_provider.h

@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/sexpr/format.h"
 #include "kernel/expr.h"
+#include "util/message_definitions.h"
 
 namespace lean {
-typedef pair<unsigned, unsigned> pos_info; //!< Line and column information
 /**
    \brief Abstract class for providing expression position information (line number and column).
 */

src/library/message_buffer.h

@@ -11,16 +11,10 @@ Author: Gabriel Ebner
 #include "util/exception.h"
 #include "util/name_set.h"
 #include "library/messages.h"
+#include "util/message_definitions.h"
 
 namespace lean {
 
-typedef uint64 period;
-
-struct message_bucket_id {
-    name m_bucket;
-    period m_version;
-};
-
 class info_manager;
 
 class message_buffer {

src/library/mt_task_queue.h

@@ -15,6 +15,7 @@ Author: Gabriel Ebner
 #include "util/optional.h"
 #include "library/io_state.h"
 #include "library/task_queue.h"
+#include "library/message_buffer.h"
 
 namespace lean {
 

src/library/task_helper.cpp

@@ -5,9 +5,10 @@ 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/trace.h"
+#include "library/message_builder.h"
 #include "library/task_helper.h"
+#include "library/message_buffer.h"
 
 namespace lean {
 

src/library/task_queue.cpp

@@ -6,6 +6,7 @@ Author: Gabriel Ebner
 */
 #include <string>
 #include "library/task_queue.h"
+#include "library/message_buffer.h"
 
 namespace lean {
 

src/library/task_queue.h

@@ -12,7 +12,7 @@ Author: Gabriel Ebner
 #include "util/thread.h"
 #include "util/optional.h"
 #include "util/rc.h"
-#include "library/message_buffer.h"
+#include "util/message_definitions.h"
 
 namespace lean {
 

src/util/message_definitions.h

@@ -0,0 +1,23 @@
+/*
+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 <utility>
+#include "util/name.h"
+#include "util/int64.h"
+
+namespace lean {
+
+typedef pair<unsigned, unsigned> pos_info; //!< Line and column information
+
+typedef uint64 period;
+
+struct message_bucket_id {
+    name m_bucket;
+    period m_version;
+};
+
+}