diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-30 21:31:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-30 21:31:12 +0000 |
commit | 5ab0f03e947ce6b81df2b30a48b300b72100100e (patch) | |
tree | 54dc654e6860174976c8d0def8da6b2a454695e6 /src | |
parent | f28bab562105548413cfca93de5c9b047157a076 (diff) |
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.)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_template.h | 14 |
1 files changed, 5 insertions, 9 deletions
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; @@ -706,12 +706,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. */ bool d_printTypes; @@ -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); |