diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 11:53:00 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 11:53:00 -0700 |
| commit | 4b7ef1b817fe00bc32294b75797e7e264e2edbdd (patch) | |
| tree | afaa7e469ea904e7bc5b17efaeb19c36ed6657b4 /Source/Dafny | |
| parent | 75e436019003604ea3118a13ccd9b6ea079c643f (diff) | |
Move indentation of error messages to the ConsoleErrorReporter
This indentation is just needed by CLI-based clients
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Reporting.cs | 5 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/QuantifiersCollection.cs | 3 |
2 files changed, 5 insertions, 3 deletions
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);
}
}
|