From c80094ecb0101406599cb9b1a169e2e6e03ff6e7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 27 Feb 2015 14:24:22 -0800 Subject: Removed Util/VS2010 folder, which has been superseded by DafnyExtension years ago --- Util/VS2010/Dafny/DafnyLanguageService.sln | 20 -- .../Dafny/DafnyLanguageService/Configuration.cs | 24 -- .../DafnyLanguageService.csproj | 179 ---------- .../DafnyLanguageService/GlobalSuppressions.cs | 11 - Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 389 --------------------- Util/VS2010/Dafny/DafnyLanguageService/Guids.cs | 13 - .../Integration/AuthoringScope.cs | 66 ---- .../Integration/Configuration.cs | 116 ------ .../Integration/Declaration.cs | 30 -- .../Integration/Declarations.cs | 56 --- .../Integration/IASTResolver.cs | 13 - .../Integration/IronyLanguageService.cs | 373 -------------------- .../Integration/IronyViewFilter.cs | 42 --- .../Integration/LineScanner.cs | 58 --- .../DafnyLanguageService/Integration/Method.cs | 20 -- .../DafnyLanguageService/Integration/Methods.cs | 50 --- .../DafnyLanguageService/Integration/Package.cs | 130 ------- .../DafnyLanguageService/Integration/Resolver.cs | 50 --- .../DafnyLanguageService/Integration/Source.cs | 41 --- .../IronyLanguageServicePackage.cs | 90 ----- Util/VS2010/Dafny/DafnyLanguageService/Key.snk | Bin 596 -> 0 bytes .../Properties/AssemblyInfo.cs | 36 -- .../DafnyLanguageService/Resources.Designer.cs | 63 ---- .../Dafny/DafnyLanguageService/Resources.resx | 130 ------- .../Dafny/DafnyLanguageService/Resources/Irony.dll | Bin 236032 -> 0 bytes .../Dafny/DafnyLanguageService/VSPackage.resx | 129 ------- .../source.extension.vsixmanifest | 27 -- Util/VS2010/Dafny/StartDafny.bat | 10 - 28 files changed, 2166 deletions(-) delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService.sln delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Guids.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Key.snk delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources.resx delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest delete mode 100644 Util/VS2010/Dafny/StartDafny.bat (limited to 'Util') 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 @@ - - - - Debug - AnyCPU - 9.0.30729 - 2.0 - Library - Properties - Demo.DafnyLanguageService - DafnyLanguageService - True - Key.snk - v4.0 - {66E611EE-84D8-4EB9-9A33-164A53E00553} - - - 4.0 - - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - true - AllRules.ruleset - - - - False - Resources\Irony.dll - - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll - - - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll - - - - False - True - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll - - - - - - False - ..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll - - - - - - - - - - - - - - - - - - - - - - - - - - - True - True - Resources.resx - - - - - - - - ResXFileCodeGenerator - Resources.Designer.cs - Designer - - - true - Designer - - - - - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Microsoft Visual Basic PowerPacks 10.0 - true - - - False - Windows Installer 3.1 - true - - - - - true - true - - - - - \ 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=" | "<=" | "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 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 colorableItems = new List(); - - public static IList 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 definitions = new Dictionary(); - - 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 - { - 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 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 declarations; - public Declarations(IList 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 FindCompletions(object result, int line, int col); - IList FindMembers(object result, int line, int col); - string FindQuickInfo(object result, int line, int col); - IList 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(); - } - 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); - } - - /// - /// Called to determine if the given location can have a breakpoint applied to it. - /// - /// The IVsTextBuffer object containing the source file. - /// The line number where the breakpoint is to be set. - /// The offset into the line where the breakpoint is to be set. - /// - /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the - /// breakpoint can be set. - /// - /// - /// 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). - /// - /// - /// - /// 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. - /// - /// - /// 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. - /// - /// - /// 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. - /// - /// - /// The base method returns E_NOTIMPL. - /// - /// - 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 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 methods; - public Methods(IList 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 FindCompletions(object result, int line, int col) - { - // Used for intellisense. - List declarations = new List(); - - // 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 FindMembers(object result, int line, int col) - { - List members = new List(); - - return members; - } - - public string FindQuickInfo(object result, int line, int col) - { - return "unknown"; - } - - public IList FindMethods(object result, int line, int col, string name) - { - return new List(); - } - - #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 braces; - public IList 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 -{ - /// - /// 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. - /// - // 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 - { - /// - /// 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. - /// - public DafnyLanguageService() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); - } - - - - ///////////////////////////////////////////////////////////////////////////// - // Overriden Package Implementation - #region Package Members - - /// - /// 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. - /// - 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 deleted file mode 100644 index f80a4ceb..00000000 Binary files a/Util/VS2010/Dafny/DafnyLanguageService/Key.snk and /dev/null differ 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 @@ -//------------------------------------------------------------------------------ -// -// 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. -// -//------------------------------------------------------------------------------ - -namespace Demo { - using System; - - - /// - /// A strongly-typed resource class, for looking up localized strings, etc. - /// - // 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() { - } - - /// - /// Returns the cached ResourceManager instance used by this class. - /// - [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; - } - } - - /// - /// Overrides the current thread's CurrentUICulture property for all - /// resource lookups using this strongly typed resource class. - /// - [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 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll b/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll deleted file mode 100644 index e2021a72..00000000 Binary files a/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll and /dev/null differ 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 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - Paste PLK Here - - - Dafny - - - Dafny Programming Language - - \ 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 @@ - - - - - DafnyService - Microsoft Research - 1.0 - Information about my package - 1033 - - - - Pro - VST_All - - - - - - - - - - DafnyService.pkgdef - - - 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 -- cgit v1.2.3