From 5ab0f03e947ce6b81df2b30a48b300b72100100e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 30 Nov 2012 21:31:12 +0000 Subject: [PATCH] change detection/handling of output language more reasonably; fixes a nagging bug Tim found in API examples (this commit was certified error- and warning-free by the test-and-commit script.) --- examples/api/Makefile | 4 ++++ src/expr/expr_template.h | 14 +++++--------- 2 files changed, 9 insertions(+), 9 deletions(-) create mode 100644 examples/api/Makefile diff --git a/examples/api/Makefile b/examples/api/Makefile new file mode 100644 index 000000000..8e5dcfd21 --- /dev/null +++ b/examples/api/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = examples/api + +include $(topdir)/Makefile.subdir diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 6cbaae4cb..1ca0e9b35 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -654,7 +654,7 @@ public: l = options::defaultExprDepth(); } if(l == 0) { - l = s_defaultPrintDepth; + return s_defaultPrintDepth; } } return l; @@ -705,12 +705,6 @@ class CVC4_PUBLIC ExprPrintTypes { */ static const int s_iosIndex; - /** - * The default printtypes setting, for ostreams that haven't yet had a - * printtypes() applied to them. - */ - static const int s_defaultPrintTypes = false; - /** * When this manipulator is used, the setting is stored here. */ @@ -882,8 +876,10 @@ public: if(l <= 0 || l > language::output::LANG_MAX) { // if called from outside the library, we may not have options // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable. - l = s_defaultOutputLanguage + 1; + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. + return OutputLanguage(s_defaultOutputLanguage); } } return OutputLanguage(l - 1); -- 2.30.2