Cleanup indentation of trigger warnings

3 files changed, 9 insertions, 7 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 01bceeb7..aa008e36 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -138,12 +138,12 @@ namespace Microsoft.Dafny.Triggers {
       var indent = addHeader ? "   " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed

 

       if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie

-        msg.AppendFormat("  Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 

+        msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 

         // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy)

         // FIXME typeQuantifier?

       } else {

         if (addHeader) {

-          msg.AppendFormat("  For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();

+          msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();

         }

 

         foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger

@@ -154,16 +154,16 @@ namespace Microsoft.Dafny.Triggers {
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);

 

 #if QUANTIFIER_WARNINGS

-        string WARN = DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "; //FIXME set unicodeoutput in extension

+        string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); //FIXME set unicodeoutput in extension

         if (!q.CandidateTerms.Any()) {

           errorLevel = ErrorLevel.Warning;

-          msg.Append(indent).Append(WARN).AppendLine("No terms found to trigger on.");

+          msg.Append(WARN).AppendLine("No terms found to trigger on.");

         } else if (!q.Candidates.Any()) {

           errorLevel = ErrorLevel.Warning;

-          msg.Append(indent).Append(WARN).AppendLine("No trigger covering all quantified variables found.");

+          msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");

         } else if (!q.CouldSuppressLoops && !q.AllowsLoops) {

           errorLevel = ErrorLevel.Warning;

-          msg.Append(indent).Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");

+          msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");

         }

 #endif

       }

diff --git a/Test/dafny0/TriggerInPredicate.dfy b/Test/dafny0/TriggerInPredicate.dfy
index 3f2eac2c..b9c372dc 100644
--- a/Test/dafny0/TriggerInPredicate.dfy
+++ b/Test/dafny0/TriggerInPredicate.dfy
@@ -3,7 +3,7 @@
 

 predicate A(x: bool, y: bool) { x }

 

-predicate B(x: bool, z: bool) { forall y {:trigger A(x, y) } :: A(x, y) && z }

+predicate B(x: bool, z: bool) { forall y {:trigger A(x, y)} :: A(x, y) && z }

 

 // Inlining is disabled here to prevent pollution of the trigger in B

 method C() requires B(true || false, true) {}

diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect
index 7f6e0268..1cbd4034 100644
--- a/Test/dafny0/TriggerInPredicate.dfy.expect
+++ b/Test/dafny0/TriggerInPredicate.dfy.expect
@@ -1,3 +1,5 @@
+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}.

+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}.

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.