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, 12 insertions, 0 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4f9488a3..65554a1e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -421,6 +421,8 @@ namespace Microsoft.Boogie {
     public string CVC4ExecutablePath = null;

     public int KInductionDepth = -1;

 

+    public bool PrettyPrint = true;

+

     public enum ProverWarnings {

       None,

       Stdout,

@@ -741,6 +743,13 @@ namespace Microsoft.Boogie {
           }

           return true;

 

+        case "pretty":

+          int val = 1;

+          if (ps.GetNumericArgument(ref val, 2)) {

+            PrettyPrint = val == 1;

+          } 

+          return true;

+

         case "OwickiGries":

           if (ps.ConfirmArgumentCount(1)) {

               OwickiGriesDesugaredOutputFile = args[ps.i];

@@ -1657,6 +1666,9 @@ namespace Microsoft.Boogie {
 

   /print:<file>  : print Boogie program after parsing it

                    (use - as <file> to print to console)

+  /pretty:<n>

+                0 - print each Boogie statement on one line (faster).

+                1 (default) - pretty-print with some line breaks.

   /printWithUniqueIds : print augmented information that uniquely

                    identifies variables

   /printUnstructured : with /print option, desugars all structured statements