diff options
author | 2014-07-28 16:04:00 +0530 | |
---|---|---|
committer | 2014-07-28 16:04:00 +0530 | |
commit | ca5d2c31be76c51bb00ad5253c1ded75c404642c (patch) | |
tree | 3d61506171cad499682297ea9c4fba6445f742d8 /Source/Core/Util.cs | |
parent | 5c5ece158229ad33f36afed8af3b5e47d99987f1 (diff) |
Helper procedures
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);
|