From 4b7ef1b817fe00bc32294b75797e7e264e2edbdd Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 11:53:00 -0700 Subject: Move indentation of error messages to the ConsoleErrorReporter This indentation is just needed by CLI-based clients --- Source/Dafny/Reporting.cs | 5 ++++- Source/Dafny/Triggers/QuantifiersCollection.cs | 3 +-- 2 files changed, 5 insertions(+), 3 deletions(-) (limited to 'Source/Dafny') diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 63ec520a..4cfbf20e 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -143,7 +143,10 @@ namespace Microsoft.Dafny { } public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { - if (base.Message(source, level, tok, msg)) { + if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) { + // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI + msg = msg.Replace(Environment.NewLine, Environment.NewLine + " "); + ConsoleColor previousColor = Console.ForegroundColor; Console.ForegroundColor = ColorForLevel(level); Console.WriteLine(ErrorToString(level, tok, msg)); diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index ec2f1777..e2afa2ee 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -171,8 +171,7 @@ namespace Microsoft.Dafny.Triggers { } if (msg.Length > 0) { - // Extra indent added to make it easier to distinguish multiline error messages - var msgStr = msg.ToString().Replace(Environment.NewLine, Environment.NewLine + " ").TrimEnd("\r\n ".ToCharArray()); + var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray()); reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr); } } -- cgit v1.2.3