michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Remove verbosity.cpp, verbosity message channel should not be a global.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-19 18:17:43 -07:00
parent f5e0150db3
commit eba4172a0c
3 changed files with 1 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/util/CMakeLists.txt
View file

@ -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)

31
src/util/verbosity.cpp
View file

@ -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;
}
}

16
src/util/verbosity.h
View file

@ -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 } }
}