change detection/handling of output language more reasonably; fixes a nagging bug...

(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 (file)
index 0000000..8e5dcfd
--- /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 6cbaae4cbce333888e8b363f1deeb214acb753c1..1ca0e9b35eeff00bcd64e6ef54e0595b746b4cbd 100644 (file)
--- 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);