summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 16:00:35 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-19 16:00:35 -0700
commit2f5d59592c5930c32039855824cc49983f643641 (patch)
treea13c8bfa6b6d2b29feeb00c7f7645fd3c498a5ff
parent8823b0e75fbf0460ddea5e10f9ee61f5fa171b44 (diff)
Enable unicode output in the VS extension
-rw-r--r--Source/Dafny/Triggers/QuantifiersCollection.cs2
-rw-r--r--Source/DafnyExtension/DafnyDriver.cs1
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs2
3 files changed, 3 insertions, 2 deletions
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index ecc193fc..a6340f10 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -156,7 +156,7 @@ namespace Microsoft.Dafny.Triggers {
AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);
#if QUANTIFIER_WARNINGS
- string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); //FIXME set unicodeoutput in extension
+ string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");
if (!q.CandidateTerms.Any()) {
errorLevel = ErrorLevel.Warning;
msg.Append(WARN).AppendLine("No terms found to trigger on.");
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 36664a9b..30b0bd52 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -40,6 +40,7 @@ namespace DafnyLanguage
options.ErrorTrace = 0;
options.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);
options.ModelViewFile = "-";
+ options.UnicodeOutput = true;
Dafny.DafnyOptions.Install(options);
// Read additional options from DafnyOptions.txt
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 0ce68809..22706338 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -403,7 +403,7 @@ namespace DafnyLanguage
chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
}
- static TaskErrorCategory CategoryConversion(ErrorCategory cat) //CLEMENT: We've lost that info
+ static TaskErrorCategory CategoryConversion(ErrorCategory cat)
{
switch (cat)
{