From eba4172a0c74c651fcf93f4cf8b0a8a2d306a01e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Aug 2013 18:17:43 -0700
Subject: [PATCH] Remove verbosity.cpp, verbosity message channel should not be
 a global.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/CMakeLists.txt |  3 +--
 src/util/verbosity.cpp  | 31 -------------------------------
 src/util/verbosity.h    | 16 ----------------
 3 files changed, 1 insertion(+), 49 deletions(-)
 delete mode 100644 src/util/verbosity.cpp
 delete mode 100644 src/util/verbosity.h

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index ffeb8257b4..603ab62589 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,3 +1,2 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
-  verbosity.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
-  safe_arith.cpp)
+  interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp)
diff --git a/src/util/verbosity.cpp b/src/util/verbosity.cpp
deleted file mode 100644
index f63f1d8f3b..0000000000
--- a/src/util/verbosity.cpp
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "verbosity.h"
-
-namespace lean {
-
-unsigned g_verbosity_level = 0;
-
-void set_verbosity_level(unsigned lvl) {
-    g_verbosity_level = lvl;
-}
-
-unsigned get_verbosity_level() {
-    return g_verbosity_level;
-}
-
-static std::ostream* g_verbose_stream = &std::cerr;
-
-void set_verbose_stream(std::ostream& str) {
-    g_verbose_stream = &str;
-}
-
-std::ostream& verbose_stream() {
-    return *g_verbose_stream;
-}
-
-}
diff --git a/src/util/verbosity.h b/src/util/verbosity.h
deleted file mode 100644
index 298611a80e..0000000000
--- a/src/util/verbosity.h
+++ /dev/null
@@ -1,16 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <iostream>
-
-namespace lean {
-void          set_verbosity_level(unsigned lvl);
-unsigned      get_verbosity_level();
-std::ostream& verbose_stream();
-void          set_verbose_stream(std::ostream& s);
-#define lean_verbose(LVL, CODE) { if (get_verbosity_level() >= LVL) { CODE } }
-}