Helper procedures

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