From 0e6fa10f4ae4bfe4ac74ca12041e0aaa23713319 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 9 Oct 2015 16:07:50 +0200
Subject: [PATCH] Printer improvements

- Ensuring always has braces
- No parens printed for function/method calls with 0 args
---
 .../scala/leon/purescala/PrettyPrinter.scala  | 24 ++++++++++++++-----
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 895250023..0453fb9a1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -101,7 +101,9 @@ class PrettyPrinter(opts: PrinterOptions,
             |$body"""
 
       case Ensuring(body, post) =>
-        p"""|$body ensuring {
+        p"""| {
+            |  $body
+            |} ensuring {
             |  $post
             |}"""
 
@@ -190,7 +192,11 @@ class PrettyPrinter(opts: PrinterOptions,
             case FunctionInvocation(tfd, _)     if tfd.fd.isSynthetic => false
             case other => true
           }
-          p"($presentArgs)"
+
+          val requireParens = presentArgs.nonEmpty || args.nonEmpty
+          if (requireParens) {
+            p"($presentArgs)"
+          }
         }
 
       case BinaryMethodCall(a, op, b) =>
@@ -207,7 +213,11 @@ class PrettyPrinter(opts: PrinterOptions,
             case FunctionInvocation(tfd, _)     if tfd.fd.isSynthetic => false
             case other => true
           }
-          p"($presentArgs)"
+
+          val requireParens = presentArgs.nonEmpty || args.nonEmpty
+          if (requireParens) {
+            p"($presentArgs)"
+          }
         }
 
       case FunctionInvocation(TypedFunDef(fd, tps), args) =>
@@ -222,7 +232,10 @@ class PrettyPrinter(opts: PrinterOptions,
             case FunctionInvocation(tfd, _)     if tfd.fd.isSynthetic => false
             case other => true
           }
-          p"($presentArgs)"
+          val requireParens = presentArgs.nonEmpty || args.nonEmpty
+          if (requireParens) {
+            p"($presentArgs)"
+          }
         }
 
       case Application(caller, args) =>
@@ -563,7 +576,7 @@ class PrettyPrinter(opts: PrinterOptions,
     case LetDef(_, bd) => Seq(bd)
     case Require(_, bd) => Seq(bd)
     case IfExpr(_, t, e) => Seq(t, e) // If always has braces anyway
-    case Ensuring(_, pred) => Seq(pred)
+    case Ensuring(bd, pred) => Seq(bd, pred)
     case _ => Seq()
   }
 
@@ -591,7 +604,6 @@ class PrettyPrinter(opts: PrinterOptions,
   protected def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
     case (pa: PrettyPrintable, _) => pa.printRequiresParentheses(within)
     case (_, None) => false
-    case (me: MatchExpr, Some(_ :Ensuring)) => true
     case (_, Some(_: Ensuring)) => false
     case (_, Some(_: Assert)) => false
     case (_, Some(_: Require)) => false
-- 
GitLab