diff options
Diffstat (limited to 'Source/Core/Util.cs')
-rw-r--r-- | Source/Core/Util.cs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 75cb25aa..0a2e5a22 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -252,6 +252,11 @@ namespace Microsoft.Boogie { }
}
+ public TokenTextWriter(string filename)
+ : this(filename, false)
+ {
+ }
+
public TokenTextWriter(string filename, bool pretty)
: base() {
Contract.Requires(filename != null);
@@ -288,6 +293,11 @@ namespace Microsoft.Boogie { this.writer = writer;
}
+ public TokenTextWriter(TextWriter writer)
+ : this(writer, false)
+ {
+ }
+
public TokenTextWriter(TextWriter writer, bool pretty)
: base() {
Contract.Requires(writer != null);
|