From 9bdf1355af20c4dd2b97ea9bc5f34cc20fbdde0f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 5 Oct 2011 19:03:23 +0000
Subject: [PATCH] minor visibility fixes

---
 src/expr/node.h   |  5 +++++
 src/util/output.h | 29 ++++++++++++++++-------------
 2 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/src/expr/node.h b/src/expr/node.h
index 0f4b55d4a..9d852f195 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -52,6 +52,11 @@ class NodeManager;
 template <bool ref_count>
 class NodeTemplate;
 
+// For some reason these are instantiated with different visibility in different modules??
+// Fix by making their instantiations explicit, here.
+template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<false> const& t) CVC4_PUBLIC;
+template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<true> const& t) CVC4_PUBLIC;
+
 /**
  * Exception thrown during the type-checking phase, it can be
  * thrown by node.getType().
diff --git a/src/util/output.h b/src/util/output.h
index da1efe68a..8a90ef136 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -112,19 +112,7 @@ public:
   operator std::ostream&() { return isConnected() ? *d_os : null_os; }
 
   template <class T>
-  CVC4ostream& operator<<(T const& t) {
-    if(d_os != NULL) {
-      if(d_firstColumn) {
-        d_firstColumn = false;
-        long indent = d_os->iword(s_indentIosIndex);
-        for(long i = 0; i < indent; ++ i) {
-          d_os = &(*d_os << s_tab);
-        }
-      }
-      d_os = &(*d_os << t);
-    }
-    return *this;
-  }
+  CVC4ostream& operator<<(T const& t) CVC4_PUBLIC;
 
   // support manipulators, endl, etc..
   CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
@@ -164,6 +152,21 @@ inline CVC4ostream& pop(CVC4ostream& stream) {
   return stream;
 }
 
+template <class T>
+CVC4ostream& CVC4ostream::operator<<(T const& t) {
+  if(d_os != NULL) {
+    if(d_firstColumn) {
+      d_firstColumn = false;
+      long indent = d_os->iword(s_indentIosIndex);
+      for(long i = 0; i < indent; ++i) {
+        d_os = &(*d_os << s_tab);
+      }
+    }
+    d_os = &(*d_os << t);
+  }
+  return *this;
+}
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
-- 
2.30.2