Skip to content

Commit

Permalink
Fix options for 'dafny resolve' (dafny-lang#3227)
Browse files Browse the repository at this point in the history
Fixes dafny-lang#3218

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer authored Dec 20, 2022
1 parent 84d201f commit d12b627
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 6 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/Options/CommonOptionBag.cs
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ Note that quantifier variable domains (<- <Domain>) are available in both syntax
ArgumentHelpName = "language"
};

public static readonly Option<bool> UnicodeCharacters = new("--unicode-char",
public static readonly Option<bool> UnicodeCharacters = new("--unicode-char", () => false,
@"
false - The char type represents any UTF-16 code unit.
true - The char type represents any Unicode scalar value.".TrimStart());
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/Options/ICommandSpec.cs
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,13 @@ static ICommandSpec() {
public static Argument<IEnumerable<FileInfo>> FilesArgument { get; }

public static IReadOnlyList<Option> VerificationOptions = new Option[] {
CommonOptionBag.RelaxDefiniteAssignment,
BoogieOptionBag.VerificationTimeLimit,
CommonOptionBag.VerifyIncludedFiles,
CommonOptionBag.ManualLemmaInduction,
CommonOptionBag.SolverPath,
CommonOptionBag.DisableNonLinearArithmetic,
BoogieOptionBag.BoogieArguments,
}.ToList();

public static IReadOnlyList<Option> ExecutionOptions = new Option[] {
Expand All @@ -55,15 +58,12 @@ static ICommandSpec() {
BoogieOptionBag.Cores,
CommonOptionBag.Libraries,
CommonOptionBag.Plugin,
BoogieOptionBag.BoogieArguments,
CommonOptionBag.Prelude,
CommonOptionBag.RelaxDefiniteAssignment,
Function.FunctionSyntaxOption,
CommonOptionBag.QuantifierSyntax,
CommonOptionBag.WarnShadowing,
CommonOptionBag.WarnMissingConstructorParenthesis,
PrintStmt.TrackPrintEffectsOption,
CommonOptionBag.DisableNonLinearArithmetic,
CommonOptionBag.UnicodeCharacters,
});

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyLanguageServer/ServerCommand.cs
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,9 @@ related locations
GhostIndicators,
LineVerificationStatus,
VerifySnapshots,
BoogieOptionBag.VerificationTimeLimit,
CommonOptionBag.EnforceDeterminism,
}.Concat(ICommandSpec.CommonOptions);
}.Concat(ICommandSpec.VerificationOptions).
Concat(ICommandSpec.CommonOptions);

public Command Create() {
var command = new Command("server", "Start the Dafny language server");
Expand Down

0 comments on commit d12b627

Please sign in to comment.