diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index ce98b7456..561812db0 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1 +1 @@ -add_library(util trace.cpp debug.cpp name.cpp exception.cpp) +add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp) diff --git a/src/util/verbosity.cpp b/src/util/verbosity.cpp new file mode 100644 index 000000000..53ec8e271 --- /dev/null +++ b/src/util/verbosity.cpp @@ -0,0 +1,31 @@ +/* +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 new file mode 100644 index 000000000..d564b9325 --- /dev/null +++ b/src/util/verbosity.h @@ -0,0 +1,18 @@ +/* +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 + +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 } } +} + +