Add DafnyOptions.txt, and have the Dafny Visual Studio extension read command-line options from DafnyOptions.txt during initialization. DafnyOptions.txt gets built into the VSIX file and is installed as part of the Dafny Visual Studio extension.

3 files changed, 29 insertions, 1 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 5dd6d8ab..5b8cc943 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -41,7 +41,25 @@ namespace DafnyLanguage
         options.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);

         options.ModelViewFile = "-";

         Dafny.DafnyOptions.Install(options);

-        options.ApplyDefaultOptions();

+

+        // Read additional options from DafnyOptions.txt

+        string codebase = Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

+        string optionsFilePath = Path.Combine(codebase, "DafnyOptions.txt");

+        if (File.Exists(optionsFilePath)) {

+          var optionsReader = new StreamReader(new FileStream(optionsFilePath, FileMode.Open, FileAccess.Read));

+          List<string> args = new List<string>();

+          while (true) {

+            string line = optionsReader.ReadLine();

+            if (line == null) break;

+            line = line.Trim();

+            if (line.Length == 0 || line.StartsWith("//")) continue;

+            args.Add(line);

+          }

+          optionsReader.Close();

+          CommandLineOptions.Clo.Parse(args.ToArray());

+        } else {

+          options.ApplyDefaultOptions();

+        }

 

         ExecutionEngine.printer = new DummyPrinter();

         ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 05bcc503..843c1528 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -116,6 +116,7 @@
     <Reference Include="Provers.SMTLib">

       <HintPath>..\..\..\boogie\Binaries\Provers.SMTLib.dll</HintPath>

     </Reference>

+    <Reference Include="System.IO.Compression.FileSystem" />

     <Reference Include="VCExpr">

       <HintPath>..\..\..\boogie\Binaries\VCExpr.dll</HintPath>

     </Reference>

@@ -183,6 +184,9 @@
     <Compile Include="..\version.cs" />

   </ItemGroup>

   <ItemGroup>

+    <Content Include="DafnyOptions.txt">

+      <IncludeInVSIX>true</IncludeInVSIX>

+    </Content>

     <Content Include="DafnyPrelude.bpl">

       <IncludeInVSIX>true</IncludeInVSIX>

     </Content>

@@ -220,6 +224,9 @@
       <Install>false</Install>

     </BootstrapperPackage>

   </ItemGroup>

+  <ItemGroup>

+    <WCFMetadata Include="Service References\" />

+  </ItemGroup>

   <PropertyGroup>

     <UseCodebase>true</UseCodebase>

   </PropertyGroup>

diff --git a/Source/DafnyExtension/DafnyOptions.txt b/Source/DafnyExtension/DafnyOptions.txt
new file mode 100644
index 00000000..e19fe525
--- /dev/null
+++ b/Source/DafnyExtension/DafnyOptions.txt
@@ -0,0 +1,3 @@
+// DafnyLanguageService.vsix copies this file to the Dafny Visual Studio Extension directory

+// Each line contains one command-line argument to the Dafny Visual Studio Extension

+// Blank lines and lines beginning with "//" are ignored