From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 30 Nov 2012 21:31:12 +0000 (+0000)
Subject: change detection/handling of output language more reasonably; fixes a nagging bug... 
X-Git-Tag: cvc5-1.0.0~7514
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ab0f03e947ce6b81df2b30a48b300b72100100e;p=cvc5.git

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

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