diff options
| author |  Rustan Leino <unknown> | 2015-02-27 14:24:22 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-02-27 14:24:22 -0800 |
| commit | c80094ecb0101406599cb9b1a169e2e6e03ff6e7 (patch) | |
| tree | adf6cb17592c38fbdee0592197b59b1c845876cc /Util | |
| parent | d77f0e32ce017b00573d5fff9929470d8c2a9830 (diff) | |
Removed Util/VS2010 folder, which has been superseded by DafnyExtension years ago
Diffstat (limited to 'Util')
28 files changed, 0 insertions, 2166 deletions
diff --git a/Util/VS2010/Dafny/DafnyLanguageService.sln b/Util/VS2010/Dafny/DafnyLanguageService.sln deleted file mode 100644 index d900cbb5..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService.sln +++ /dev/null @@ -1,20 +0,0 @@ -
-Microsoft Visual Studio Solution File, Format Version 11.00
-# Visual Studio 2010
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyLanguageService", "DafnyLanguageService\DafnyLanguageService.csproj", "{66E611EE-84D8-4EB9-9A33-164A53E00553}"
-EndProject
-Global
- GlobalSection(SolutionConfigurationPlatforms) = preSolution
- Debug|Any CPU = Debug|Any CPU
- Release|Any CPU = Release|Any CPU
- EndGlobalSection
- GlobalSection(ProjectConfigurationPlatforms) = postSolution
- {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.Build.0 = Release|Any CPU
- EndGlobalSection
- GlobalSection(SolutionProperties) = preSolution
- HideSolutionNode = FALSE
- EndGlobalSection
-EndGlobal
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs deleted file mode 100644 index f32c75ab..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs +++ /dev/null @@ -1,24 +0,0 @@ -using System;
-using System.Collections.Generic;
-using Microsoft.VisualStudio.Package;
-using Microsoft.VisualStudio.TextManager.Interop;
-
-namespace Demo
-{
- public static partial class Configuration
- {
- public const string Name = "Dafny";
- public const string FormatList = "Dafny File (*.dfy)\n*.dfy";
-
- static Configuration()
- {
- // default colors - currently, these need to be declared
- CreateColor("Keyword", COLORINDEX.CI_BLUE, COLORINDEX.CI_USERTEXT_BK);
- CreateColor("Comment", COLORINDEX.CI_DARKGREEN, COLORINDEX.CI_USERTEXT_BK);
- CreateColor("Identifier", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK);
- CreateColor("String", COLORINDEX.CI_MAROON, COLORINDEX.CI_USERTEXT_BK);
- CreateColor("Number", COLORINDEX.CI_RED, COLORINDEX.CI_USERTEXT_BK);
- CreateColor("Text", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK);
- }
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj b/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj deleted file mode 100644 index 175c12dc..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj +++ /dev/null @@ -1,179 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.30729</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Demo.DafnyLanguageService</RootNamespace>
- <AssemblyName>DafnyLanguageService</AssemblyName>
- <SignAssembly>True</SignAssembly>
- <AssemblyOriginatorKeyFile>Key.snk</AssemblyOriginatorKeyFile>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <ProjectGuid>{66E611EE-84D8-4EB9-9A33-164A53E00553}</ProjectGuid>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>4.0</OldToolsVersion>
- <UpgradeBackupLocation>
- </UpgradeBackupLocation>
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile />
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <RunCodeAnalysis>true</RunCodeAnalysis>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <ItemGroup>
- <Reference Include="Irony, Version=1.0.0.0, Culture=neutral, PublicKeyToken=ca48ace7223ead47, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>Resources\Irony.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.OLE.Interop" />
- <Reference Include="Microsoft.VisualStudio.Package.LanguageService.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.10.0">
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.Interop" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
- <SpecificVersion>False</SpecificVersion>
- <EmbedInteropTypes>True</EmbedInteropTypes>
- <HintPath>C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath>
- </Reference>
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" />
- <Reference Include="Microsoft.VisualStudio.TextManager.Interop" />
- <Reference Include="Microsoft.VisualStudio.TextManager.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
- <SpecificVersion>False</SpecificVersion>
- <HintPath>..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll</HintPath>
- </Reference>
- <Reference Include="System" />
- <Reference Include="System.Data" />
- <Reference Include="System.Design" />
- <Reference Include="System.Drawing" />
- <Reference Include="System.Windows.Forms" />
- <Reference Include="System.Xml" />
- </ItemGroup>
- <ItemGroup>
- <Compile Include="Configuration.cs" />
- <Compile Include="Grammar.cs" />
- <Compile Include="Guids.cs" />
- <Compile Include="Integration\AuthoringScope.cs" />
- <Compile Include="Integration\Configuration.cs" />
- <Compile Include="Integration\Declaration.cs" />
- <Compile Include="Integration\Declarations.cs" />
- <Compile Include="Integration\IASTResolver.cs" />
- <Compile Include="Integration\IronyViewFilter.cs" />
- <Compile Include="Integration\IronyLanguageService.cs" />
- <Compile Include="Integration\LineScanner.cs" />
- <Compile Include="Integration\Method.cs" />
- <Compile Include="Integration\Methods.cs" />
- <Compile Include="Integration\Package.cs" />
- <Compile Include="Integration\Resolver.cs" />
- <Compile Include="Integration\Source.cs" />
- <Compile Include="Resources.Designer.cs">
- <AutoGen>True</AutoGen>
- <DesignTime>True</DesignTime>
- <DependentUpon>Resources.resx</DependentUpon>
- </Compile>
- <Compile Include="GlobalSuppressions.cs" />
- <Compile Include="IronyLanguageServicePackage.cs" />
- <Compile Include="Properties\AssemblyInfo.cs" />
- </ItemGroup>
- <ItemGroup>
- <EmbeddedResource Include="Resources.resx">
- <Generator>ResXFileCodeGenerator</Generator>
- <LastGenOutput>Resources.Designer.cs</LastGenOutput>
- <SubType>Designer</SubType>
- </EmbeddedResource>
- <EmbeddedResource Include="VSPackage.resx">
- <MergeWithCTO>true</MergeWithCTO>
- <SubType>Designer</SubType>
- </EmbeddedResource>
- </ItemGroup>
- <ItemGroup>
- <Content Include="Resources\Irony.dll" />
- <None Include="source.extension.vsixmanifest" />
- </ItemGroup>
- <ItemGroup>
- <None Include="Key.snk" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.VisualBasic.PowerPacks.10.0">
- <Visible>False</Visible>
- <ProductName>Microsoft Visual Basic PowerPacks 10.0</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </ItemGroup>
- <PropertyGroup>
- <!--
- To specify a different registry root to register your package, uncomment the TargetRegistryRoot
- tag and specify a registry root in it.
- <TargetRegistryRoot></TargetRegistryRoot>
- -->
- <RegisterOutputPackage>true</RegisterOutputPackage>
- <RegisterWithCodebase>true</RegisterWithCodebase>
- </PropertyGroup>
- <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
- <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
-</Project>
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs b/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs deleted file mode 100644 index f0857cbb..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs +++ /dev/null @@ -1,11 +0,0 @@ -// This file is used by Code Analysis to maintain SuppressMessage
-// attributes that are applied to this project. Project-level
-// suppressions either have no target or are given a specific target
-// and scoped to a namespace, type, member, etc.
-//
-// To add a suppression to this file, right-click the message in the
-// Error List, point to "Suppress Message(s)", and click "In Project
-// Suppression File". You do not need to add suppressions to this
-// file manually.
-
-[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")]
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs deleted file mode 100644 index d8ec579a..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ /dev/null @@ -1,389 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using Irony.Parsing;
-
-namespace Demo
-{
- [Language("Dafny", "1.0", "Dafny Programming Language")]
- public class Grammar : Irony.Parsing.Grammar
- {
- public Grammar() {
- #region 1. Terminals
- NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");
-
- IdentifierTerminal ident = new IdentifierTerminal("Identifier", "'_?", "'_?");
-
- StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
-
- this.MarkReservedWords( // NOTE: these keywords must also appear once more below
- "class", "ghost", "static", "var", "method", "constructor", "colemma", "datatype", "codatatype",
- "iterator", "type",
- "assert", "assume", "new", "this", "object", "refines",
- "abstract", "module", "import", "as", "default", "opened",
- "if", "then", "else", "while", "invariant",
- "break", "label", "return", "yield", "print",
- "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",
- "bool", "nat", "int", "false", "true", "null",
- "function", "predicate", "copredicate", "free",
- "in", "forall", "exists",
- "seq", "set", "map", "multiset", "array", "array2", "array3",
- "match", "case",
- "fresh", "old", "choose", "where", "calc"
- );
-
- StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);
-
- Terminal dot = ToTerm(".", "dot");
- Terminal less = ToTerm("<");
- Terminal greater = ToTerm(">");
- Terminal arrow = ToTerm("=>");
- Terminal LBracket = ToTerm("[");
- Terminal RBracket = ToTerm("]");
- Terminal LParen = ToTerm("(");
- Terminal RParen = ToTerm(")");
- Terminal RCurly = ToTerm("}");
- Terminal LCurly = ToTerm("{");
- Terminal LMb = ToTerm("<[");
- Terminal RMb = ToTerm("]>");
- Terminal comma = ToTerm(",");
- Terminal semicolon = ToTerm(";");
- Terminal colon = ToTerm(":");
-
- #endregion
-
- #region 2. Non-terminals
- #region 2.1 Expressions
- NonTerminal expression = new NonTerminal("Expr");
- NonTerminal BinOp = new NonTerminal("BinOp");
- NonTerminal LUnOp = new NonTerminal("LUnOp");
- NonTerminal RUnOp = new NonTerminal("RUnOp");
-
- NonTerminal ArrayConstructor = new NonTerminal("ArrayConstructor");
- NonTerminal MObjectConstructor = new NonTerminal("MObjectConstructor");
- NonTerminal MObjectList = new NonTerminal("MObjectList");
- #endregion
-
- #region 2.2 QualifiedName
- //Expression List: expr1, expr2, expr3, ..
- NonTerminal expressionList = new NonTerminal("ExprList");
- NonTerminal identList = new NonTerminal("identList");
- //A name in form: a.b.c().d[1,2].e ....
- NonTerminal NewStmt = new NonTerminal("NewStmt");
- NonTerminal NewArrStmt = new NonTerminal("NewArrStmt");
- NonTerminal QualifiedName = new NonTerminal("QualifiedName");
- NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix");
- NonTerminal ArrayExpression = new NonTerminal("ArrayExpression");
- NonTerminal FunctionExpression = new NonTerminal("FunctionExpression");
- NonTerminal selectExpr = new NonTerminal("selectExpr");
- #endregion
-
- #region 2.3 Statement
- NonTerminal Condition = new NonTerminal("Condition");
-
- NonTerminal Statement = new NonTerminal("Statement");
- NonTerminal Statements = new NonTerminal("Statements");
-
- //Block
- NonTerminal blockStatement = new NonTerminal("CompoundStatement");
- #endregion
-
- #region 2.4 Program and Functions
- NonTerminal Prog = new NonTerminal("Prog");
- NonTerminal anything = new NonTerminal("anything"); // temporary hack
- NonTerminal declaration = new NonTerminal("declaration");
- NonTerminal classDecl = new NonTerminal("class decl");
- NonTerminal memberDecl = new NonTerminal("member decl");
- NonTerminal fieldDecl = new NonTerminal("field declaration");
- NonTerminal idType = new NonTerminal("identifier type");
- NonTerminal typeDecl = new NonTerminal("type reference");
- NonTerminal methodDecl = new NonTerminal("method declaration");
- NonTerminal formalParameters = new NonTerminal("formals");
- NonTerminal methodSpec = new NonTerminal("method spec");
- NonTerminal formalsList = new NonTerminal("ParamaterListOpt");
- NonTerminal functionDecl = new NonTerminal("function declaration");
- NonTerminal predicateDecl = new NonTerminal("predicate declaration");
- NonTerminal invariantDecl = new NonTerminal("invariant declaration");
- NonTerminal Semi = new NonTerminal("semi");
- NonTerminal Rhs = new NonTerminal("right-hand side");
- NonTerminal FieldInit = new NonTerminal("field init");
- NonTerminal FieldInits = new NonTerminal("field inits");
- NonTerminal installBounds = new NonTerminal("installBounds");
- NonTerminal localVarStmt = new NonTerminal("localVarStmt");
- NonTerminal evalstate = new NonTerminal("evalstate");
- NonTerminal channelDecl = new NonTerminal("channel declaration");
- NonTerminal loopSpec = new NonTerminal("loop specification");
- NonTerminal rdPermArg = new NonTerminal("rdPermArg");
- #endregion
-
- #endregion
-
- #region 3. BNF rules
-
- Semi.Rule = semicolon;
-
- #region 3.1 Expressions
- selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName;
- evalstate.Rule =
- ident + ToTerm(".") +
- (ToTerm("acquire")
- | "release"
- | "fork" + FunctionExpression
- )
- ;
- rdPermArg.Rule = ToTerm("*") | expression;
-
- expression.Rule = ToTerm("true")
- | "false"
- | "null"
- | "maxlock"
- | "lockbottom"
- | "this"
- | "result"
- | s
- | n
- | QualifiedName
- // The following is needed: to parse "A<B ..." either as comparison or as beginning of GenericsPostfix
- | QualifiedName + less + expression
- //| QualifiedName + less + QualifiedName + greater
- //| NewStmt
- | NewArrStmt
- | ArrayExpression
- | FunctionExpression
- | ArrayConstructor
- | MObjectConstructor
- | expression + BinOp + expression
- | LUnOp + expression
- | expression + RUnOp
- | LMb + declaration.Star() + RMb
- | LParen + expression + RParen
- | ToTerm("unfolding") + expression + "in" + expression
- | ToTerm("acc") + "(" + selectExpr + (("," + expression) | Empty) + ")"
- | ToTerm("old") + "(" + expression + ")"
- | ToTerm("eval") + "(" + evalstate + "," + expression + ")"
- | ToTerm("credit") + "(" + expression + "," + expression + ")"
- | ToTerm("credit") + "(" + expression + ")"
- | expression + PreferShiftHere() + "?" + expression + ":" + expression
- | ToTerm("rd") +
- (ToTerm("holds") + "(" + expression + ")"
- | "(" + selectExpr + rdPermArg.Q() + ")"
- )
-
- ;
- expressionList.Rule = MakePlusRule(expressionList, comma, expression);
- identList.Rule = MakePlusRule(identList, comma, ident);
- NewStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LParen + expressionList.Q() + RParen;
- NewArrStmt.Rule = "new" + QualifiedName + GenericsPostfix.Q() + LBracket + expressionList.Q() + RBracket;
- BinOp.Rule = ToTerm("+") | "-" | "*" | "/" | "%" | "^" | "&" | "|"
- | "&&" | "||" | "==" | "!=" | greater | less
- | ">=" | "<=" | "is"
- | "=" | "+=" | "-="
- | "."
- | "==>" | "<==>" | "<<"
- | "=" // this is for datatype declarations, not an operator
- ;
-
- LUnOp.Rule = ToTerm("-") | "~" | "!";
- RUnOp.Rule = ToTerm("++") | "--";
-
- ArrayConstructor.Rule = LBracket + expressionList + RBracket;
- MObjectConstructor.Rule = LBracket + ident + arrow + expression + MObjectList.Star() + RBracket;
- MObjectList.Rule = comma + ident + arrow + expression;
- #endregion
-
- #region 3.2 QualifiedName
- ArrayExpression.Rule = QualifiedName + LBracket + expressionList + RBracket;
- FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen;
-
- QualifiedName.Rule = ident | QualifiedName + dot + ident;
-
-
- GenericsPostfix.Rule = less + QualifiedName + greater;
-
- //ExprList.Rule = Expr.Plus(comma);
- #endregion
-
- #region 3.3 Statement
- Condition.Rule = LParen + expression + RParen;
- installBounds.Rule
- = "installBounds"
- //= ToTerm("between") + expressionList + "and" + expressionList
- //| "below" + expressionList
- //| "below" + expressionList + "above" + expressionList
- //| "above" + expressionList
- //| "above" + expressionList + "below" + expressionList
- ;
- FieldInit.Rule
- = ident + ":=" + expression
- ;
- FieldInits.Rule = MakeStarRule(FieldInits, ToTerm(","), FieldInit);
- Rhs.Rule
- = ToTerm("new") + ident
- | ToTerm("new") + ident + "{" + FieldInits + "}"
- | ToTerm("new") + ident + installBounds
- | ToTerm("new") + ident + "{" + FieldInits + "}" + installBounds
- | expression
- ;
- localVarStmt.Rule
- = idType + ":=" + Rhs + Semi
- | idType + Semi
- ;
- loopSpec.Rule
- = ToTerm("invariant") + expression + Semi
- | "lockchange" + expressionList + Semi
- ;
-
-
-
- Statement.Rule = Semi
- | "if" + Condition + Statement
- | "if" + Condition + Statement + PreferShiftHere() + "else" + Statement
- | "while" + Condition + loopSpec.Star() + Statement
- | "for" + LParen + expression.Q() + Semi + expression.Q() + Semi + expression.Q() + RParen + Statement
- | blockStatement
- | expression + Semi
- | "break" + Semi
- | QualifiedName + ":=" + Rhs
-
- | "var" + localVarStmt
-
- | "assert" + expression + Semi
- | "assume" + expression + Semi
-
- ;
- Statements.Rule = MakeStarRule(Statements, null, Statement);
- blockStatement.Rule = LCurly + Statements + RCurly;
-
-
- #endregion
-
- #region 3.4 Prog
- Prog.Rule = anything.Star() + Eof;
-
- anything.Rule
- = ToTerm("class")
- | "ghost"
- | "static"
- | "var"
- | "method"
- | "constructor"
- | "colemma"
- | "datatype"
- | "codatatype"
- | "type"
- | "iterator"
- | "assert"
- | "assume"
- | "new"
- | "this"
- | "object"
- | "refines"
- | "abstract"
- | "module"
- | "import"
- | "default"
- | "opened"
- | "as"
- | "if"
- | "then"
- | "else"
- | "while"
- | "invariant"
- | "break"
- | "label"
- | "return"
- | "yield"
- | "calc"
- | "print"
- | "returns"
- | "yields"
- | "requires"
- | "ensures"
- | "modifies"
- | "reads"
- | "decreases"
- | "bool"
- | "nat"
- | "int"
- | "false"
- | "true"
- | "null"
- | "function"
- | "predicate"
- | "copredicate"
- | "free"
- | "in"
- | "forall"
- | "exists"
- | "seq"
- | "set"
- | "map"
- | "multiset"
- | "array"
- | "array2"
- | "array3"
- | "match"
- | "case"
- | "fresh"
- | "old"
- | "choose"
- | "where"
- | ident
- | "}"
- | "{"
- | "("
- | ")"
- | "["
- | "]"
- | ","
- | ":"
- | ";"
- | "=" // this is for datatype declarations, not an operator
- | "."
- | "`"
- | "=="
- | "!="
- | "<"
- | "<="
- | ">="
- | ">"
- | "=>"
- | ":="
- | "+"
- | "-"
- | "*"
- | "/"
- | "%"
- | "!!"
- | "|"
- | "!"
- | "&&"
- | "||"
- | "==>"
- | "<==>"
- | "#"
- | n
- | stringLiteral
- ;
-
- Terminal Comment = new CommentTerminal("Comment", "/*", "*/");
- NonGrammarTerminals.Add(Comment);
- Terminal LineComment = new CommentTerminal("LineComment", "//", "\n");
- NonGrammarTerminals.Add(LineComment);
- #endregion
- #endregion
-
- #region 4. Set starting symbol
- this.Root = Prog; // Set grammar root
- #endregion
-
- #region 5. Operators precedence
- // not used
- #endregion
-
- #region 6. Punctuation symbols
- RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";");
- #endregion
- }
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs b/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs deleted file mode 100644 index 61ea05d4..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs +++ /dev/null @@ -1,13 +0,0 @@ -using System;
-
-namespace Demo
-{
- static class GuidList
- {
- public const string guidIronyLanguageServiceString = "1F9687D0-937C-428E-ACFF-A7622A14100C";
- public const string guidIronyLanguageServicePkgString = "F85E7515-4CA6-42A5-86E0-D2312AE91D23";
- public const string guidIronyLanguageServiceCmdSetString = "68251AE3-0205-4FC9-8B12-D4C3EA9F8D6C";
-
- public static readonly Guid guidIronyLanguageServiceCmdSet = new Guid(guidIronyLanguageServiceCmdSetString);
- };
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs deleted file mode 100644 index 9a49dbe4..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs +++ /dev/null @@ -1,66 +0,0 @@ -using System;
-using System.Collections.Generic;
-using Microsoft.VisualStudio;
-using Microsoft.VisualStudio.TextManager.Interop;
-using Microsoft.VisualStudio.Package;
-
-namespace Demo
-{
- public class AuthoringScope : Microsoft.VisualStudio.Package.AuthoringScope
- {
- public AuthoringScope(object parseResult)
- {
- this.parseResult = parseResult;
-
- // how should this be set?
- this.resolver = new Resolver();
- }
-
- object parseResult;
- IASTResolver resolver;
-
- // ParseReason.QuickInfo
- public override string GetDataTipText(int line, int col, out TextSpan span)
- {
- span = new TextSpan();
- return null;
- }
-
- // ParseReason.CompleteWord
- // ParseReason.DisplayMemberList
- // ParseReason.MemberSelect
- // ParseReason.MemberSelectAndHilightBraces
- public override Microsoft.VisualStudio.Package.Declarations GetDeclarations(IVsTextView view, int line, int col, TokenInfo info, ParseReason reason)
- {
- IList<Declaration> declarations;
- switch (reason)
- {
- case ParseReason.CompleteWord:
- declarations = resolver.FindCompletions(parseResult, line, col);
- break;
- case ParseReason.DisplayMemberList:
- case ParseReason.MemberSelect:
- case ParseReason.MemberSelectAndHighlightBraces:
- declarations = resolver.FindMembers(parseResult, line, col);
- break;
- default:
- throw new ArgumentException("reason");
- }
-
- return new Declarations(declarations);
- }
-
- // ParseReason.GetMethods
- public override Microsoft.VisualStudio.Package.Methods GetMethods(int line, int col, string name)
- {
- return new Methods(resolver.FindMethods(parseResult, line, col, name));
- }
-
- // ParseReason.Goto
- public override string Goto(VSConstants.VSStd97CmdID cmd, IVsTextView textView, int line, int col, out TextSpan span)
- {
- span = new TextSpan();
- return null;
- }
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs deleted file mode 100644 index f7412393..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs +++ /dev/null @@ -1,116 +0,0 @@ -using System;
-using System.Collections.Generic;
-using Microsoft.VisualStudio.Package;
-using Microsoft.VisualStudio.TextManager.Interop;
-
-namespace Demo
-{
- public static partial class Configuration
- {
- public static Grammar Grammar = new Grammar();
- static List<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> colorableItems = new List<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem>();
-
- public static IList<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> ColorableItems
- {
- get { return colorableItems; }
- }
-
- public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background)
- {
- return CreateColor(name, foreground, background, false, false);
- }
-
- public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough)
- {
- colorableItems.Add(new ColorableItem(name, foreground, background, bold, strikethrough));
- return (TokenColor)colorableItems.Count;
- }
-
- public static void ColorToken(string tokenName, TokenType type, TokenColor color, TokenTriggers trigger)
- {
- definitions[tokenName] = new TokenDefinition(type, color, trigger);
- }
-
- public static TokenDefinition GetDefinition(string tokenName)
- {
- TokenDefinition result;
- return definitions.TryGetValue(tokenName, out result) ? result : defaultDefinition;
- }
-
- private static TokenDefinition defaultDefinition = new TokenDefinition(TokenType.Text, TokenColor.Text, TokenTriggers.None);
- private static Dictionary<string, TokenDefinition> definitions = new Dictionary<string, TokenDefinition>();
-
- public struct TokenDefinition
- {
- public TokenDefinition(TokenType type, TokenColor color, TokenTriggers triggers)
- {
- this.TokenType = type;
- this.TokenColor = color;
- this.TokenTriggers = triggers;
- }
-
- public TokenType TokenType;
- public TokenColor TokenColor;
- public TokenTriggers TokenTriggers;
- }
- }
-
- public class ColorableItem : Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem
- {
- private string displayName;
- private COLORINDEX background;
- private COLORINDEX foreground;
- private uint fontFlags = (uint)FONTFLAGS.FF_DEFAULT;
-
- public ColorableItem(string displayName, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough)
- {
- this.displayName = displayName;
- this.background = background;
- this.foreground = foreground;
-
- if (bold)
- this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_BOLD;
- if (strikethrough)
- this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_STRIKETHROUGH;
- }
-
- #region IVsColorableItem Members
- public int GetDefaultColors(COLORINDEX[] piForeground, COLORINDEX[] piBackground)
- {
- if (null == piForeground)
- {
- throw new ArgumentNullException("piForeground");
- }
- if (0 == piForeground.Length)
- {
- throw new ArgumentOutOfRangeException("piForeground");
- }
- piForeground[0] = foreground;
-
- if (null == piBackground)
- {
- throw new ArgumentNullException("piBackground");
- }
- if (0 == piBackground.Length)
- {
- throw new ArgumentOutOfRangeException("piBackground");
- }
- piBackground[0] = background;
-
- return Microsoft.VisualStudio.VSConstants.S_OK;
- }
-
- public int GetDefaultFontFlags(out uint pdwFontFlags)
- {
- pdwFontFlags = this.fontFlags;
- return Microsoft.VisualStudio.VSConstants.S_OK;
- }
-
- public int GetDisplayName(out string pbstrName)
- {
- pbstrName = displayName;
- return Microsoft.VisualStudio.VSConstants.S_OK;
- }
- #endregion
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs deleted file mode 100644 index c0fda5ca..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs +++ /dev/null @@ -1,30 +0,0 @@ -using System;
-using System.Collections.Generic;
-
-namespace Demo
-{
- public struct Declaration : IComparable<Declaration>
- {
- public Declaration(string description, string displayText, int glyph, string name)
- {
- this.Description = description;
- this.DisplayText = displayText;
- this.Glyph = glyph;
- this.Name = name;
- }
-
- public string Description;
- public string DisplayText;
- public int Glyph;
- public string Name;
-
- #region IComparable<Declaration> Members
-
- public int CompareTo(Declaration other)
- {
- return DisplayText.CompareTo(other.DisplayText);
- }
-
- #endregion
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs deleted file mode 100644 index 98a411ce..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs +++ /dev/null @@ -1,56 +0,0 @@ -/***************************************************************************
-
-Copyright (c) Microsoft Corporation. All rights reserved.
-This code is licensed under the Visual Studio SDK license terms.
-THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF
-ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY
-IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR
-PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT.
-
-***************************************************************************/
-
-using System;
-using System.Collections.Generic;
-using System.Text;
-using Microsoft.VisualStudio.TextManager.Interop;
-using Microsoft.VisualStudio.Package;
-
-namespace Demo
-{
- public class Declarations : Microsoft.VisualStudio.Package.Declarations
- {
- IList<Declaration> declarations;
- public Declarations(IList<Declaration> declarations)
- {
- this.declarations = declarations;
- }
-
- public override int GetCount()
- {
- return declarations.Count;
- }
-
- public override string GetDescription(int index)
- {
- return declarations[index].Description;
- }
-
- public override string GetDisplayText(int index)
- {
- return declarations[index].DisplayText;
- }
-
- public override int GetGlyph(int index)
- {
- return declarations[index].Glyph;
- }
-
- public override string GetName(int index)
- {
- if (index >= 0)
- return declarations[index].Name;
-
- return null;
- }
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs deleted file mode 100644 index 8de1a454..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs +++ /dev/null @@ -1,13 +0,0 @@ -using System;
-using System.Collections.Generic;
-
-namespace Demo
-{
- interface IASTResolver
- {
- IList<Declaration> FindCompletions(object result, int line, int col);
- IList<Declaration> FindMembers(object result, int line, int col);
- string FindQuickInfo(object result, int line, int col);
- IList<Method> FindMethods(object result, int line, int col, string name);
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs deleted file mode 100644 index ce43e6e4..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs +++ /dev/null @@ -1,373 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Diagnostics;
-using Microsoft.VisualStudio;
-using Microsoft.VisualStudio.TextManager.Interop;
-using Microsoft.VisualStudio.Package;
-
-using Irony.Parsing;
-using Irony.Ast;
-
-using System.IO;
-
-namespace Demo
-{
- public class IronyLanguageService : Microsoft.VisualStudio.Package.LanguageService
- {
- private Grammar grammar;
- private Parser parser;
- private ParsingContext context;
-
- public IronyLanguageService()
- {
- grammar = new Grammar();
- parser = new Parser(Configuration.Grammar);
- context = new ParsingContext(parser);
- }
-
-
- #region Custom Colors
- public override int GetColorableItem(int index, out IVsColorableItem item)
- {
- if (index <= Configuration.ColorableItems.Count)
- {
- item = Configuration.ColorableItems[index - 1];
- return Microsoft.VisualStudio.VSConstants.S_OK;
- }
- else
- {
- throw new ArgumentNullException("index");
- }
- }
-
- public override int GetItemCount(out int count)
- {
- count = Configuration.ColorableItems.Count;
- return Microsoft.VisualStudio.VSConstants.S_OK;
- }
- #endregion
-
- #region MPF Accessor and Factory specialisation
- private LanguagePreferences preferences;
- public override LanguagePreferences GetLanguagePreferences()
- {
- if (this.preferences == null)
- {
- this.preferences = new LanguagePreferences(this.Site,
- typeof(IronyLanguageService).GUID,
- this.Name);
- this.preferences.Init();
- }
-
- return this.preferences;
- }
-
- public override Microsoft.VisualStudio.Package.Source CreateSource(IVsTextLines buffer)
- {
- return new Source(this, buffer, this.GetColorizer(buffer));
- }
-
- private IScanner scanner;
- public override IScanner GetScanner(IVsTextLines buffer)
- {
- if (scanner == null)
- this.scanner = new LineScanner(grammar);
-
- return this.scanner;
- }
- #endregion
-
- public override void OnIdle(bool periodic)
- {
- // from IronPythonLanguage sample
- // this appears to be necessary to get a parse request with ParseReason = Check?
- Source src = (Source)GetSource(this.LastActiveTextView);
- if (src != null && src.LastParseTime >= Int32.MaxValue >> 12)
- {
- src.LastParseTime = 0;
- }
- base.OnIdle(periodic);
- }
-
- public override Microsoft.VisualStudio.Package.AuthoringScope ParseSource(ParseRequest req)
- {
- Debug.Print("ParseSource at ({0}:{1}), reason {2}", req.Line, req.Col, req.Reason);
- Source source = (Source)this.GetSource(req.FileName);
- switch (req.Reason)
- {
- case ParseReason.Check:
- // This is where you perform your syntax highlighting.
- // Parse entire source as given in req.Text.
- // Store results in the AuthoringScope object.
- var parsed = parser.Parse(req.Text, req.FileName);
- var root = parsed.Root;
- if (root != null) {
-
- AstNode node = (AstNode)root.AstNode;
- source.ParseResult = node;
- }
-
- // Used for brace matching.
- TokenStack braces = parser.Context.OpenBraces;
- foreach (Token brace in braces) {
- if (brace.OtherBrace == null) continue;
- TextSpan openBrace = new TextSpan();
- openBrace.iStartLine = brace.Location.Line;
- openBrace.iStartIndex = brace.Location.Column;
- openBrace.iEndLine = brace.Location.Line;
- openBrace.iEndIndex = openBrace.iStartIndex + brace.Length;
-
- TextSpan closeBrace = new TextSpan();
- closeBrace.iStartLine = brace.OtherBrace.Location.Line;
- closeBrace.iStartIndex = brace.OtherBrace.Location.Column;
- closeBrace.iEndLine = brace.OtherBrace.Location.Line;
- closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length;
-
- if (source.Braces == null) {
- source.Braces = new List<TextSpan[]>();
- }
- source.Braces.Add(new TextSpan[2] { openBrace, closeBrace });
- }
-
- if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) {
- foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) {
- TextSpan span = new TextSpan();
- span.iStartLine = span.iEndLine = error.Location.Line - 1;
- span.iStartIndex = error.Location.Column;
- span.iEndIndex = error.Location.Position;
- req.Sink.AddError(req.FileName, error.Message, span, Severity.Error);
- }
- } else { // parse looks okay, send it to Dafny.
- if (!File.Exists(@"C:\tmp\StartDafny.bat")) {
- AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartDafny.bat");
- } else {
-
- // From: http://dotnetperls.com/process-redirect-standard-output
- // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx)
- //
- // Setup the process with the ProcessStartInfo class.
- //
- ProcessStartInfo start = new ProcessStartInfo();
- start.FileName = @"cmd.exe";
- start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name.
- start.UseShellExecute = false;
- start.RedirectStandardInput = true;
- start.RedirectStandardOutput = true;
- start.CreateNoWindow = true;
- //start.WindowStyle = ProcessWindowStyle.Minimized; // need this or else you see the window pop up
- //
- // Start the process.
- //
- using (Process process = Process.Start(start)) {
- //
- // Push the file contents to the new process
- //
- StreamWriter myStreamWriter = process.StandardInput;
- myStreamWriter.WriteLine(req.Text);
- myStreamWriter.Close();
- //
- // Read in all the text from the process with the StreamReader.
- //
- using (StreamReader reader = process.StandardOutput) {
- //string result = reader.ReadToEnd();
- //Console.Write(result);
-
- for (string line = reader.ReadLine(); line != null; line = reader.ReadLine()) {
- // the lines of interest have the form "filename(line,col): some_error_label: error_message"
- // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"
- if (line.Equals("")) continue;
- if (line.StartsWith("Dafny program verifier finished with"))
- {
- if (line.Contains("time out"))
- {
- AddErrorBecauseOfToolProblems(req, "Verification timed out.");
- }
- else
- {
- if (!line.Contains("inconclusive") && !line.Contains("out of memory"))
- {
- if (line.Contains(" 0 errors"))
- AddMessage(req, "Verification successful.");
- }
- else
- {
- AddErrorBecauseOfToolProblems(req, "Internal verification fault.");
- }
- }
- break;
- }
- string message;
- int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..."
- if (n == -1) {
- continue;
- } else {
- int m = line.IndexOf(": ", n + 3);
- if (m == -1) {
- continue;
- }
- message = line.Substring(m + 2);
- }
- line = line.Substring(0, n); // line now has the form "filename(line,col"
-
- n = line.LastIndexOf(',');
- if (n == -1) { continue; }
- var colString = line.Substring(n + 1);
- line = line.Substring(0, n); // line now has the form "filename(line"
-
- n = line.LastIndexOf('(');
- if (n == -1) { continue; }
- var lineString = line.Substring(n + 1);
-
- try {
- TextSpan span = new TextSpan();
- span.iStartLine = span.iEndLine = Int32.Parse(lineString) - 1;
- span.iStartIndex = Int32.Parse(colString) - 1;
- span.iEndIndex = span.iStartIndex + 5; // hack
- req.Sink.AddError(req.FileName, message, span, Severity.Error);
- } catch (System.FormatException) {
- continue;
- } catch (System.OverflowException) {
- continue;
- }
- }
- }
- }
- }
- }
-
- break;
-
- case ParseReason.DisplayMemberList:
- // Parse the line specified in req.Line for the two
- // tokens just before req.Col to obtain the identifier
- // and the member connector symbol.
- // Examine existing parse tree for members of the identifer
- // and return a list of members in your version of the
- // Declarations class as stored in the AuthoringScope
- // object.
- break;
-
- case ParseReason.MethodTip:
- // Parse the line specified in req.Line for the token
- // just before req.Col to obtain the name of the method
- // being entered.
- // Examine the existing parse tree for all method signatures
- // with the same name and return a list of those signatures
- // in your version of the Methods class as stored in the
- // AuthoringScope object.
- break;
-
- case ParseReason.HighlightBraces:
- case ParseReason.MemberSelectAndHighlightBraces:
- if (source.Braces != null)
- {
- foreach (TextSpan[] brace in source.Braces)
- {
- if (brace.Length == 2)
- req.Sink.MatchPair(brace[0], brace[1], 1);
- else if (brace.Length >= 3)
- req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1);
- }
- }
- break;
- }
-
- return new AuthoringScope(source.ParseResult);
- }
-
- private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg)
- {
- TextSpan span = new TextSpan();
- span.iStartLine = span.iEndLine = 0;
- span.iStartIndex = 0;
- span.iEndIndex = 0;
- req.Sink.AddError(req.FileName, msg, span, Severity.Error);
- }
- private static void AddMessage(ParseRequest req, string msg)
- {
- TextSpan span = new TextSpan();
- span.iStartLine = span.iEndLine = 0;
- span.iStartIndex = 0;
- span.iEndIndex = 1;
- req.Sink.AddError(req.FileName, msg, span, Severity.Hint);
- }
-
- /// <summary>
- /// Called to determine if the given location can have a breakpoint applied to it.
- /// </summary>
- /// <param name="buffer">The IVsTextBuffer object containing the source file.</param>
- /// <param name="line">The line number where the breakpoint is to be set.</param>
- /// <param name="col">The offset into the line where the breakpoint is to be set.</param>
- /// <param name="pCodeSpan">
- /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the
- /// breakpoint can be set.
- /// </param>
- /// <returns>
- /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given
- /// position or returns an error code (the validation is deferred until the debug engine is loaded).
- /// </returns>
- /// <remarks>
- /// <para>
- /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language
- /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a
- /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere
- /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this
- /// method but the span must always be set. The example shows how this can be done.
- /// </para>
- /// <para>
- /// Since the language service parses the code, it generally knows what is considered code and what
- /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine.
- /// </para>
- /// <para>
- /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan.
- /// The parser examines the specified location and returns a span identifying the code at that
- /// location. If there is code at the location, the span identifying that code should be passed to
- /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your
- /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of
- /// the AuthoringSink class and returns that span in the pCodeSpan argument.
- /// </para>
- /// <para>
- /// The base method returns E_NOTIMPL.
- /// </para>
- /// </remarks>
- public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan)
- {
- // TODO: Add code to not allow breakpoints to be placed on non-code lines.
- // TODO: Refactor to allow breakpoint locations to span multiple lines.
- if (pCodeSpan != null)
- {
- pCodeSpan[0].iStartLine = line;
- pCodeSpan[0].iStartIndex = col;
- pCodeSpan[0].iEndLine = line;
- pCodeSpan[0].iEndIndex = col;
- if (buffer != null)
- {
- int length;
- buffer.GetLengthOfLine(line, out length);
- pCodeSpan[0].iStartIndex = 0;
- pCodeSpan[0].iEndIndex = length;
- }
- return VSConstants.S_OK;
- }
- else
- {
- return VSConstants.S_FALSE;
- }
- }
-
- public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView)
- {
- return new IronyViewFilter(mgr, newView);
- }
-
- public override string Name
- {
- get { return Configuration.Name; }
- }
-
- public override string GetFormatFilterList()
- {
- return Configuration.FormatList;
- }
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs deleted file mode 100644 index 55c3509e..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs +++ /dev/null @@ -1,42 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.VisualStudio.Package;
-using Microsoft.VisualStudio.TextManager.Interop;
-
-using VsCommands2K = Microsoft.VisualStudio.VSConstants.VSStd2KCmdID;
-
-namespace Demo
-{
- public class IronyViewFilter : ViewFilter
- {
- public IronyViewFilter(CodeWindowManager mgr, IVsTextView view)
- : base(mgr, view)
- {
-
- }
-
- public override void HandlePostExec(ref Guid guidCmdGroup, uint nCmdId, uint nCmdexecopt, IntPtr pvaIn, IntPtr pvaOut, bool bufferWasChanged)
- {
- if (guidCmdGroup == typeof(VsCommands2K).GUID)
- {
- VsCommands2K cmd = (VsCommands2K)nCmdId;
- switch (cmd)
- {
- case VsCommands2K.UP:
- case VsCommands2K.UP_EXT:
- case VsCommands2K.UP_EXT_COL:
- case VsCommands2K.DOWN:
- case VsCommands2K.DOWN_EXT:
- case VsCommands2K.DOWN_EXT_COL:
- Source.OnCommand(TextView, cmd, '\0');
- return;
- }
- }
-
-
- base.HandlePostExec(ref guidCmdGroup, nCmdId, nCmdexecopt, pvaIn, pvaOut, bufferWasChanged);
- }
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs deleted file mode 100644 index 966e9c43..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs +++ /dev/null @@ -1,58 +0,0 @@ -using System;
-using Microsoft.VisualStudio.Package;
-using Irony.Parsing;
-
-namespace Demo
-{
- public class LineScanner : IScanner
- {
- private Parser parser;
-
- public LineScanner(Grammar grammar)
- {
- this.parser = new Parser(grammar);
- this.parser.Context.Mode = ParseMode.VsLineScan;
- }
-
- public bool ScanTokenAndProvideInfoAboutIt(TokenInfo tokenInfo, ref int state)
- {
- // Reads each token in a source line and performs syntax coloring. It will continue to
- // be called for the source until false is returned.
- Token token = parser.Scanner.VsReadToken(ref state);
-
- // !EOL and !EOF
- if (token != null && token.Terminal != Grammar.CurrentGrammar.Eof && token.Category != TokenCategory.Error)
- {
- tokenInfo.StartIndex = token.Location.Position;
- tokenInfo.EndIndex = tokenInfo.StartIndex + token.Length - 1;
- if (token.EditorInfo != null) {
- tokenInfo.Color = (Microsoft.VisualStudio.Package.TokenColor)token.EditorInfo.Color;
- tokenInfo.Type = (Microsoft.VisualStudio.Package.TokenType)token.EditorInfo.Type;
- }
-
- if (token.KeyTerm != null && token.KeyTerm.EditorInfo != null)
- {
- tokenInfo.Trigger =
- (Microsoft.VisualStudio.Package.TokenTriggers)token.KeyTerm.EditorInfo.Triggers;
- }
- else
- {
- if (token.EditorInfo != null) {
- tokenInfo.Trigger =
- (Microsoft.VisualStudio.Package.TokenTriggers)token.EditorInfo.Triggers;
- }
- }
-
- return true;
- }
-
- return false;
- }
-
- public void SetSource(string source, int offset)
- {
- // Stores line of source to be used by ScanTokenAndProvideInfoAboutIt.
- parser.Scanner.VsSetSource(source, offset);
- }
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs deleted file mode 100644 index c5071612..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs +++ /dev/null @@ -1,20 +0,0 @@ -using System;
-using System.Collections.Generic;
-
-namespace Demo
-{
- public struct Method
- {
- public string Name;
- public string Description;
- public string Type;
- public IList<Parameter> Parameters;
- }
-
- public struct Parameter
- {
- public string Name;
- public string Display;
- public string Description;
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs deleted file mode 100644 index 1d7c124f..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs +++ /dev/null @@ -1,50 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Text;
-using Microsoft.VisualStudio.TextManager.Interop;
-using Microsoft.VisualStudio.Package;
-
-namespace Demo
-{
- public class Methods : Microsoft.VisualStudio.Package.Methods
- {
- IList<Method> methods;
- public Methods(IList<Method> methods)
- {
- this.methods = methods;
- }
-
- public override int GetCount()
- {
- return methods.Count;
- }
-
- public override string GetName(int index)
- {
- return methods[index].Name;
- }
-
- public override string GetDescription(int index)
- {
- return methods[index].Description;
- }
-
- public override string GetType(int index)
- {
- return methods[index].Type;
- }
-
- public override int GetParameterCount(int index)
- {
- return (methods[index].Parameters == null) ? 0 : methods[index].Parameters.Count;
- }
-
- public override void GetParameterInfo(int index, int paramIndex, out string name, out string display, out string description)
- {
- Parameter parameter = methods[index].Parameters[paramIndex];
- name = parameter.Name;
- display = parameter.Display;
- description = parameter.Description;
- }
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs deleted file mode 100644 index dc1244d6..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs +++ /dev/null @@ -1,130 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Text;
-using System.Runtime.InteropServices;
-using Microsoft.VisualStudio.OLE.Interop;
-using MPF = Microsoft.VisualStudio.Package;
-using System.ComponentModel.Design;
-
-namespace Demo
-{
- public class IronyPackage : Microsoft.VisualStudio.Shell.Package, IOleComponent
- {
- uint componentID = 0;
- public IronyPackage()
- {
- ServiceCreatorCallback callback = new ServiceCreatorCallback(
- delegate(IServiceContainer container, Type serviceType)
- {
- if (typeof(IronyLanguageService) == serviceType)
- {
- IronyLanguageService language = new IronyLanguageService();
- language.SetSite(this);
-
- // register for idle time callbacks
- IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager;
- if (componentID == 0 && mgr != null)
- {
- OLECRINFO[] crinfo = new OLECRINFO[1];
- crinfo[0].cbSize = (uint)Marshal.SizeOf(typeof(OLECRINFO));
- crinfo[0].grfcrf = (uint)_OLECRF.olecrfNeedIdleTime |
- (uint)_OLECRF.olecrfNeedPeriodicIdleTime;
- crinfo[0].grfcadvf = (uint)_OLECADVF.olecadvfModal |
- (uint)_OLECADVF.olecadvfRedrawOff |
- (uint)_OLECADVF.olecadvfWarningsOff;
- crinfo[0].uIdleTimeInterval = 300;
- int hr = mgr.FRegisterComponent(this, crinfo, out componentID);
- }
-
- return language;
- }
- else
- {
- return null;
- }
- });
-
- // proffer the LanguageService
- (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true);
- }
-
- protected override void Dispose(bool disposing)
- {
- try
- {
- if (componentID != 0)
- {
- IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager;
- if (mgr != null)
- {
- mgr.FRevokeComponent(componentID);
- }
- componentID = 0;
- }
- }
- finally
- {
- base.Dispose(disposing);
- }
- }
-
- #region IOleComponent Members
- public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked)
- {
- return 1;
- }
-
- public int FDoIdle(uint grfidlef)
- {
- IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService;
-
- if (ls != null)
- {
- ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0);
- }
-
- return 0;
- }
-
- public int FPreTranslateMessage(MSG[] pMsg)
- {
- return 0;
- }
-
- public int FQueryTerminate(int fPromptUser)
- {
- return 1;
- }
-
- public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam)
- {
- return 1;
- }
-
- public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved)
- {
- return IntPtr.Zero;
- }
-
- public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved)
- {
- }
-
- public void OnAppActivate(int fActive, uint dwOtherThreadID)
- {
- }
-
- public void OnEnterState(uint uStateID, int fEnter)
- {
- }
-
- public void OnLoseActivation()
- {
- }
-
- public void Terminate()
- {
- }
- #endregion
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs deleted file mode 100644 index 9f6ddeba..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs +++ /dev/null @@ -1,50 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Text;
-using Irony.Parsing;
-
-namespace Demo
-{
- public class Resolver : Demo.IASTResolver
- {
- #region IASTResolver Members
-
-
- public IList<Demo.Declaration> FindCompletions(object result, int line, int col)
- {
- // Used for intellisense.
- List<Demo.Declaration> declarations = new List<Demo.Declaration>();
-
- // Add keywords defined by grammar
- foreach (KeyTerm key in Configuration.Grammar.KeyTerms.Values)
- {
- if(key.OptionIsSet(TermOptions.IsKeyword))
- {
- declarations.Add(new Declaration("", key.Name, 206, key.Name));
- }
- }
-
- declarations.Sort();
- return declarations;
- }
-
- public IList<Demo.Declaration> FindMembers(object result, int line, int col)
- {
- List<Demo.Declaration> members = new List<Demo.Declaration>();
-
- return members;
- }
-
- public string FindQuickInfo(object result, int line, int col)
- {
- return "unknown";
- }
-
- public IList<Demo.Method> FindMethods(object result, int line, int col, string name)
- {
- return new List<Demo.Method>();
- }
-
- #endregion
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs deleted file mode 100644 index 418bec01..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs +++ /dev/null @@ -1,41 +0,0 @@ -/***************************************************************************
-
-Copyright (c) Microsoft Corporation. All rights reserved.
-This code is licensed under the Visual Studio SDK license terms.
-THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF
-ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY
-IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR
-PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT.
-
-***************************************************************************/
-
-using System;
-using System.Collections.Generic;
-using System.Text;
-using Microsoft.VisualStudio.TextManager.Interop;
-using Microsoft.VisualStudio.Package;
-
-namespace Demo
-{
- public class Source : Microsoft.VisualStudio.Package.Source
- {
- public Source(LanguageService service, IVsTextLines textLines, Colorizer colorizer)
- : base(service, textLines, colorizer)
- {
- }
-
- private object parseResult;
- public object ParseResult
- {
- get { return parseResult; }
- set { parseResult = value; }
- }
-
- private IList<TextSpan[]> braces;
- public IList<TextSpan[]> Braces
- {
- get { return braces; }
- set { braces = value; }
- }
- }
-}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs deleted file mode 100644 index 29371f91..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs +++ /dev/null @@ -1,90 +0,0 @@ -// VsPkg.cs : Implementation of IronyLanguageService
-//
-
-using System;
-using System.Diagnostics;
-using System.Globalization;
-using System.Runtime.InteropServices;
-using System.ComponentModel.Design;
-using Microsoft.Win32;
-using Microsoft.VisualStudio.Shell.Interop;
-using Microsoft.VisualStudio.OLE.Interop;
-using Microsoft.VisualStudio.Shell;
-
-namespace Demo
-{
- /// <summary>
- /// This is the class that implements the package exposed by this assembly.
- ///
- /// The minimum requirement for a class to be considered a valid package for Visual Studio
- /// is to implement the IVsPackage interface and register itself with the shell.
- /// This package uses the helper classes defined inside the Managed Package Framework (MPF)
- /// to do it: it derives from the Package class that provides the implementation of the
- /// IVsPackage interface and uses the registration attributes defined in the framework to
- /// register itself and its components with the shell.
- /// </summary>
- // This attribute tells the registration utility (regpkg.exe) that this class needs
- // to be registered as package.
- [PackageRegistration(UseManagedResourcesOnly = true)]
- // A Visual Studio component can be registered under different regitry roots; for instance
- // when you debug your package you want to register it in the experimental hive. This
- // attribute specifies the registry root to use if no one is provided to regpkg.exe with
- // the /root switch.
- [DefaultRegistryRoot("Software\\Microsoft\\VisualStudio\\10.0Exp")]
- // This attribute is used to register the informations needed to show the this package
- // in the Help/About dialog of Visual Studio.
- [InstalledProductRegistration(/*false,*/ "#110", "#112", "1.0", IconResourceID = 400)]
- // This attribute will make your language service accessible by other packages installed.
- [ProvideService(typeof(IronyLanguageService))]
- // This attribute(s) associates file extensions with your language service.
- [ProvideLanguageExtension(typeof(IronyLanguageService), ".dfy")]
-
- // This attributes informs Visual Studio that this package provides a langauge service and
- // which features are implemented.
- [ProvideLanguageService(typeof(IronyLanguageService), Configuration.Name, 0,
- CodeSense = true,
- EnableCommenting = true,
- MatchBraces = true,
- MatchBracesAtCaret = true,
- ShowMatchingBrace = true,
- AutoOutlining = true)]
- // In order be loaded inside Visual Studio in a machine that has not the VS SDK installed,
- // package needs to have a valid load key (it can be requested at
- // http://msdn.microsoft.com/vstudio/extend/). This attributes tells the shell that this
- // package has a load key embedded in its resources.
- [ProvideLoadKey("Standard", "1.0", "Dafny", "Demo", 104)]
- [Guid(GuidList.guidIronyLanguageServicePkgString)]
- public sealed class DafnyLanguageService : IronyPackage
- {
- /// <summary>
- /// Default constructor of the package.
- /// Inside this method you can place any initialization code that does not require
- /// any Visual Studio service because at this point the package object is created but
- /// not sited yet inside Visual Studio environment. The place to do all the other
- /// initialization is the Initialize method.
- /// </summary>
- public DafnyLanguageService()
- {
- Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString()));
- }
-
-
-
- /////////////////////////////////////////////////////////////////////////////
- // Overriden Package Implementation
- #region Package Members
-
- /// <summary>
- /// Initialization of the package; this method is called right after the package is sited, so this is the place
- /// where you can put all the initilaization code that rely on services provided by VisualStudio.
- /// </summary>
- protected override void Initialize()
- {
- Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString()));
- base.Initialize();
-
- }
- #endregion
-
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Key.snk b/Util/VS2010/Dafny/DafnyLanguageService/Key.snk Binary files differdeleted file mode 100644 index f80a4ceb..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Key.snk +++ /dev/null diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs deleted file mode 100644 index 118d4488..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,36 +0,0 @@ -using System;
-using System.Reflection;
-using System.Resources;
-using System.Runtime.CompilerServices;
-using System.Runtime.InteropServices;
-
-// General Information about an assembly is controlled through the following
-// set of attributes. Change these attribute values to modify the information
-// associated with an assembly.
-[assembly: AssemblyTitle("Package Name")]
-[assembly: AssemblyDescription("")]
-[assembly: AssemblyConfiguration("")]
-[assembly: AssemblyCompany("Company")]
-[assembly: AssemblyProduct("Package Name")]
-[assembly: AssemblyCopyright("")]
-[assembly: AssemblyTrademark("")]
-[assembly: AssemblyCulture("")]
-[assembly: ComVisible(false)]
-[assembly: CLSCompliant(false)]
-[assembly: NeutralResourcesLanguage("en-US")]
-
-// Version information for an assembly consists of the following four values:
-//
-// Major Version
-// Minor Version
-// Build Number
-// Revision
-//
-// You can specify all the values or you can default the Revision and Build Numbers
-// by using the '*' as shown below:
-
-[assembly: AssemblyVersion("1.0.0.0")]
-[assembly: AssemblyFileVersion("1.0.0.0")]
-
-
-
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs b/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs deleted file mode 100644 index 0ca81303..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs +++ /dev/null @@ -1,63 +0,0 @@ -//------------------------------------------------------------------------------
-// <auto-generated>
-// This code was generated by a tool.
-// Runtime Version:4.0.21006.1
-//
-// Changes to this file may cause incorrect behavior and will be lost if
-// the code is regenerated.
-// </auto-generated>
-//------------------------------------------------------------------------------
-
-namespace Demo {
- using System;
-
-
- /// <summary>
- /// A strongly-typed resource class, for looking up localized strings, etc.
- /// </summary>
- // This class was auto-generated by the StronglyTypedResourceBuilder
- // class via a tool like ResGen or Visual Studio.
- // To add or remove a member, edit your .ResX file then rerun ResGen
- // with the /str option, or rebuild your VS project.
- [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")]
- [global::System.Diagnostics.DebuggerNonUserCodeAttribute()]
- [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()]
- internal class Resources {
-
- private static global::System.Resources.ResourceManager resourceMan;
-
- private static global::System.Globalization.CultureInfo resourceCulture;
-
- [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")]
- internal Resources() {
- }
-
- /// <summary>
- /// Returns the cached ResourceManager instance used by this class.
- /// </summary>
- [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]
- internal static global::System.Resources.ResourceManager ResourceManager {
- get {
- if (object.ReferenceEquals(resourceMan, null)) {
- global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("Demo.DafnyLanguageService.Resources", typeof(Resources).Assembly);
- resourceMan = temp;
- }
- return resourceMan;
- }
- }
-
- /// <summary>
- /// Overrides the current thread's CurrentUICulture property for all
- /// resource lookups using this strongly typed resource class.
- /// </summary>
- [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)]
- internal static global::System.Globalization.CultureInfo Culture {
- get {
- return resourceCulture;
- }
- set {
- resourceCulture = value;
- }
- }
- }
-}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx b/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx deleted file mode 100644 index 03fef612..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx +++ /dev/null @@ -1,130 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<!--
- VS SDK Notes: This resx file contains the resources that will be consumed directly by your package.
- For example, if you chose to create a tool window, there is a resource with ID 'CanNotCreateWindow'. This
- is used in VsPkg.cs to determine the string to show the user if there is an error when attempting to create
- the tool window.
-
- Resources that are accessed directly from your package *by Visual Studio* are stored in the VSPackage.resx
- file.
--->
-<root>
- <!--
- Microsoft ResX Schema
-
- Version 2.0
-
- The primary goals of this format is to allow a simple XML format
- that is mostly human readable. The generation and parsing of the
- various data types are done through the TypeConverter classes
- associated with the data types.
-
- Example:
-
- ... ado.net/XML headers & schema ...
- <resheader name="resmimetype">text/microsoft-resx</resheader>
- <resheader name="version">2.0</resheader>
- <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>
- <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>
- <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>
- <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>
- <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">
- <value>[base64 mime encoded serialized .NET Framework object]</value>
- </data>
- <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">
- <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>
- <comment>This is a comment</comment>
- </data>
-
- There are any number of "resheader" rows that contain simple
- name/value pairs.
-
- Each data row contains a name, and value. The row also contains a
- type or mimetype. Type corresponds to a .NET class that support
- text/value conversion through the TypeConverter architecture.
- Classes that don't support this are serialized and stored with the
- mimetype set.
-
- The mimetype is used for serialized objects, and tells the
- ResXResourceReader how to depersist the object. This is currently not
- extensible. For a given mimetype the value must be set accordingly:
-
- Note - application/x-microsoft.net.object.binary.base64 is the format
- that the ResXResourceWriter will generate, however the reader can
- read any of the formats listed below.
-
- mimetype: application/x-microsoft.net.object.binary.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.soap.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Soap.SoapFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.bytearray.base64
- value : The object must be serialized into a byte array
- : using a System.ComponentModel.TypeConverter
- : and then encoded with base64 encoding.
- -->
- <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">
- <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />
- <xsd:element name="root" msdata:IsDataSet="true">
- <xsd:complexType>
- <xsd:choice maxOccurs="unbounded">
- <xsd:element name="metadata">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" />
- </xsd:sequence>
- <xsd:attribute name="name" use="required" type="xsd:string" />
- <xsd:attribute name="type" type="xsd:string" />
- <xsd:attribute name="mimetype" type="xsd:string" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="assembly">
- <xsd:complexType>
- <xsd:attribute name="alias" type="xsd:string" />
- <xsd:attribute name="name" type="xsd:string" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="data">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />
- <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />
- <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="resheader">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" />
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
- </xsd:complexType>
- </xsd:element>
- </xsd:schema>
- <resheader name="resmimetype">
- <value>text/microsoft-resx</value>
- </resheader>
- <resheader name="version">
- <value>2.0</value>
- </resheader>
- <resheader name="reader">
- <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <resheader name="writer">
- <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <assembly alias="System.Windows.Forms" name="System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" />
-</root>
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll b/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll Binary files differdeleted file mode 100644 index e2021a72..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll +++ /dev/null diff --git a/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx b/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx deleted file mode 100644 index 68782536..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx +++ /dev/null @@ -1,129 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<root>
- <!--
- Microsoft ResX Schema
-
- Version 2.0
-
- The primary goals of this format is to allow a simple XML format
- that is mostly human readable. The generation and parsing of the
- various data types are done through the TypeConverter classes
- associated with the data types.
-
- Example:
-
- ... ado.net/XML headers & schema ...
- <resheader name="resmimetype">text/microsoft-resx</resheader>
- <resheader name="version">2.0</resheader>
- <resheader name="reader">System.Resources.ResXResourceReader, System.Windows.Forms, ...</resheader>
- <resheader name="writer">System.Resources.ResXResourceWriter, System.Windows.Forms, ...</resheader>
- <data name="Name1"><value>this is my long string</value><comment>this is a comment</comment></data>
- <data name="Color1" type="System.Drawing.Color, System.Drawing">Blue</data>
- <data name="Bitmap1" mimetype="application/x-microsoft.net.object.binary.base64">
- <value>[base64 mime encoded serialized .NET Framework object]</value>
- </data>
- <data name="Icon1" type="System.Drawing.Icon, System.Drawing" mimetype="application/x-microsoft.net.object.bytearray.base64">
- <value>[base64 mime encoded string representing a byte array form of the .NET Framework object]</value>
- <comment>This is a comment</comment>
- </data>
-
- There are any number of "resheader" rows that contain simple
- name/value pairs.
-
- Each data row contains a name, and value. The row also contains a
- type or mimetype. Type corresponds to a .NET class that support
- text/value conversion through the TypeConverter architecture.
- Classes that don't support this are serialized and stored with the
- mimetype set.
-
- The mimetype is used for serialized objects, and tells the
- ResXResourceReader how to depersist the object. This is currently not
- extensible. For a given mimetype the value must be set accordingly:
-
- Note - application/x-microsoft.net.object.binary.base64 is the format
- that the ResXResourceWriter will generate, however the reader can
- read any of the formats listed below.
-
- mimetype: application/x-microsoft.net.object.binary.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Binary.BinaryFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.soap.base64
- value : The object must be serialized with
- : System.Runtime.Serialization.Formatters.Soap.SoapFormatter
- : and then encoded with base64 encoding.
-
- mimetype: application/x-microsoft.net.object.bytearray.base64
- value : The object must be serialized into a byte array
- : using a System.ComponentModel.TypeConverter
- : and then encoded with base64 encoding.
- -->
- <xsd:schema id="root" xmlns="" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:msdata="urn:schemas-microsoft-com:xml-msdata">
- <xsd:import namespace="http://www.w3.org/XML/1998/namespace" />
- <xsd:element name="root" msdata:IsDataSet="true">
- <xsd:complexType>
- <xsd:choice maxOccurs="unbounded">
- <xsd:element name="metadata">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" />
- </xsd:sequence>
- <xsd:attribute name="name" use="required" type="xsd:string" />
- <xsd:attribute name="type" type="xsd:string" />
- <xsd:attribute name="mimetype" type="xsd:string" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="assembly">
- <xsd:complexType>
- <xsd:attribute name="alias" type="xsd:string" />
- <xsd:attribute name="name" type="xsd:string" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="data">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- <xsd:element name="comment" type="xsd:string" minOccurs="0" msdata:Ordinal="2" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" msdata:Ordinal="1" />
- <xsd:attribute name="type" type="xsd:string" msdata:Ordinal="3" />
- <xsd:attribute name="mimetype" type="xsd:string" msdata:Ordinal="4" />
- <xsd:attribute ref="xml:space" />
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="resheader">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element name="value" type="xsd:string" minOccurs="0" msdata:Ordinal="1" />
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required" />
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
- </xsd:complexType>
- </xsd:element>
- </xsd:schema>
- <resheader name="resmimetype">
- <value>text/microsoft-resx</value>
- </resheader>
- <resheader name="version">
- <value>2.0</value>
- </resheader>
- <resheader name="reader">
- <value>System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <resheader name="writer">
- <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
- </resheader>
- <data name="104" xml:space="preserve">
- <value>Paste PLK Here</value>
- </data>
- <data name="110" xml:space="preserve">
- <value>Dafny</value>
- </data>
- <data name="112" xml:space="preserve">
- <value>Dafny Programming Language</value>
- </data>
-</root>
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest b/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest deleted file mode 100644 index 58e160cd..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest +++ /dev/null @@ -1,27 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Vsix xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema" Version="1.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2010">
-
- <Identifier Id="DafnyService.MicrosoftResearch.A38156F6-63DF-4E3C-8D23-07D3DE0D3388">
- <Name>DafnyService</Name>
- <Author>Microsoft Research</Author>
- <Version>1.0</Version>
- <Description>Information about my package</Description>
- <Locale>1033</Locale>
- <!--<InstalledByMSI>false</InstalledByMSI>-->
- <SupportedProducts>
- <VisualStudio Version="10.0">
- <Edition>Pro</Edition>
- <Edition>VST_All</Edition>
- </VisualStudio>
- </SupportedProducts>
- <SupportedFrameworkRuntimeEdition MinVersion="2.0" MaxVersion="4.0" />
- </Identifier>
-
- <References/>
-
- <Content>
- <VsPackage>
- DafnyService.pkgdef
- </VsPackage>
- </Content>
-</Vsix>
diff --git a/Util/VS2010/Dafny/StartDafny.bat b/Util/VS2010/Dafny/StartDafny.bat deleted file mode 100644 index 71dc149a..00000000 --- a/Util/VS2010/Dafny/StartDafny.bat +++ /dev/null @@ -1,10 +0,0 @@ -@echo off
-echo ---------- Starting ------------ < nul >> c:\tmp\doo.out
-time < nul >> c:\tmp\doo.out
-echo. < nul >> c:\tmp\doo.out
-
-"c:\boogie\Binaries\Dafny.exe" -nologo stdin.dfy -compile:0 -timeLimit:10 %* 2>> c:\tmp\doo.out
-
-time < nul >> c:\tmp\doo.out
-echo. < nul >> c:\tmp\doo.out
-echo ---------- Done ------------ < nul >> c:\tmp\doo.out
|