Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"

When running boogie form the command line, this should be on by default.
On the other hand, the TokenTextWriter constructors and PrintBplFile now have an
argument for this, but by default it is off.

1 files changed, 96 insertions, 5 deletions

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index c14cb82e..66eefd8c 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -127,6 +127,90 @@ namespace Microsoft.Boogie {
                 "while",

         };

 

+    // "Pretty" printing: not very efficient, and not necessarily very pretty, but helps a bit 

+    private readonly bool pretty;

+    

+    // The stack of writers in a current separator-block.

+    // The string is an optional identifier that allows you

+    // to not start a new indentation for e.g. "&&" in "a && b && c".

+    // When the pretty printing is finished, this should be empty.

+    Stack<KeyValuePair<string, List<TextWriter>>> wstk;

+

+    // The original writer: where everything should finally end up.

+    TextWriter actual_writer;

+

+    public bool push(string type = null) {

+      if (pretty) {

+        if (wstk == null) {

+          wstk = new Stack<KeyValuePair<string, List<TextWriter>>>();

+          actual_writer = writer;

+        }

+        if (wstk.Count > 0 && wstk.Peek().Key == type && type != null) {

+          sep();

+          return false; // don't actually pop this thing (send this bool to pop)

+        } else {

+          wstk.Push(new KeyValuePair<string, List<TextWriter>>(type, new List<TextWriter> { }));

+          sep();

+          return true;  // this needs to be popped

+        }

+      } else {

+        return false;

+      }

+    }

+

+    public void pop(bool do_it = true) {

+      if (pretty) {

+        if (do_it) {

+          List<TextWriter> ws = wstk.Pop().Value;

+          // try to figure out if you should insert line breaks between

+          // them or print them on one single line

+          // this breaks down when there are newlines inserted

+          List<String> ss = new List<String>();

+          int len = 0;

+          foreach (TextWriter w in ws) {

+            foreach (String s in w.ToString().Split(new String[] { "\r\n", "\n" }, StringSplitOptions.None)) {

+              if (s.Length > 0) {

+                ss.Add(s);

+                len += s.Length;

+                // len = Math.Max(len, s.Length);

+              }

+            }

+          }

+          // figure out which is the next writer to use

+          List<TextWriter> tw = wstk.Count > 0 ? wstk.Peek().Value : null;

+          if (tw == null) {

+            writer = actual_writer;

+          } else {

+            writer = tw.Last();

+          }

+          // write the strings (we would like to know WHERE we are in the document here)

+          if (len > 80 /* - wstk.Count * 2 */) {

+            for (int i = 0; i < ss.Count; i++) {

+              if (i != ss.Count - 1) {

+                writer.WriteLine(ss[i]);

+                writer.Write("  ");

+              } else {

+                writer.Write(ss[i]);

+              }

+            }

+          } else {

+            foreach (String s in ss) {

+              writer.Write(s);

+            }

+          }

+        }

+      }

+    }

+

+    public void sep() {

+      if (pretty) {

+        List<TextWriter> ws = wstk.Peek().Value;

+

+        writer = new StringWriter();

+        wstk.Peek().Value.Add(writer);

+      }

+    }

+

     private IToken/*!*/ CurrentToken {

       get {

         Contract.Ensures(Contract.Result<IToken>() != null);

@@ -160,46 +244,53 @@ namespace Microsoft.Boogie {
       } else if (name.Length > 2 && name[0] == 'b' && name[1] == 'v') {

         int dummy;

         return int.TryParse(name.Substring(2), out dummy) ? "\\" + name : name;

+      } else if (name.Contains('@')) {

+        return SanitizeIdentifier(name.Replace("@", "#AT#"));

       } else {

         return name;

       }

     }

 

-    public TokenTextWriter(string filename)

+    public TokenTextWriter(string filename, bool pretty = false)

       : base() {

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = new StreamWriter(filename);

     }

 

-    public TokenTextWriter(string filename, bool setTokens)

+    public TokenTextWriter(string filename, bool setTokens, bool pretty = false)

       : base() {

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = new StreamWriter(filename);

       this.setTokens = setTokens;

     }

 

-    public TokenTextWriter(string filename, TextWriter writer, bool setTokens)

+    public TokenTextWriter(string filename, TextWriter writer, bool setTokens, bool pretty = false)

       : base() {

       Contract.Requires(writer != null);

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = writer;

       this.setTokens = setTokens;

     }

 

-    public TokenTextWriter(string filename, TextWriter writer)

+    public TokenTextWriter(string filename, TextWriter writer, bool pretty = false)

       : base() {

       Contract.Requires(writer != null);

       Contract.Requires(filename != null);

+      this.pretty = pretty;

       this.filename = filename;

       this.writer = writer;

     }

 

-    public TokenTextWriter(TextWriter writer)

+    public TokenTextWriter(TextWriter writer, bool pretty = false)

       : base() {

       Contract.Requires(writer != null);

+      this.pretty = pretty;

       this.filename = "<no file>";

       this.writer = writer;

     }