From 13c9d58997d2d40657980b1c8a9bdc9fa99485e7 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 15 Jul 2010 23:50:30 +0000 Subject: Visual Studio 2010 integration for Dafny and Chalice. See the "How to install binaries" link from the boogie.codeplex.com home page. --- Util/VS2010/Chalice/ChaliceLanguageService.sln | 20 + .../ChaliceLanguageService.csproj | 179 +++++++++ .../ChaliceLanguageService/Configuration.cs | 25 ++ .../ChaliceLanguageService/GlobalSuppressions.cs | 11 + .../Chalice/ChaliceLanguageService/Grammar.cs | 366 +++++++++++++++++ .../VS2010/Chalice/ChaliceLanguageService/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 | 335 ++++++++++++++++ .../Integration/IronyViewFilter.cs | 42 ++ .../Integration/LineScanner.cs | 58 +++ .../ChaliceLanguageService/Integration/Method.cs | 20 + .../ChaliceLanguageService/Integration/Methods.cs | 50 +++ .../ChaliceLanguageService/Integration/Package.cs | 130 ++++++ .../ChaliceLanguageService/Integration/Resolver.cs | 50 +++ .../ChaliceLanguageService/Integration/Source.cs | 41 ++ .../IronyLanguageServicePackage.cs | 91 +++++ Util/VS2010/Chalice/ChaliceLanguageService/Key.snk | Bin 0 -> 596 bytes .../Properties/AssemblyInfo.cs | 36 ++ .../ChaliceLanguageService/Resources.Designer.cs | 63 +++ .../Chalice/ChaliceLanguageService/Resources.resx | 130 ++++++ .../ChaliceLanguageService/Resources/Irony.dll | Bin 0 -> 236032 bytes .../Chalice/ChaliceLanguageService/VSPackage.resx | 129 ++++++ .../source.extension.vsixmanifest | 27 ++ Util/VS2010/Chalice/StartChalice.bat | 10 + Util/VS2010/Dafny/DafnyLanguageService.sln | 20 + .../Dafny/DafnyLanguageService/Configuration.cs | 24 ++ .../DafnyLanguageService.csproj | 179 +++++++++ .../DafnyLanguageService/GlobalSuppressions.cs | 11 + Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 445 +++++++++++++++++++++ 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 | 343 ++++++++++++++++ .../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 0 -> 596 bytes .../Properties/AssemblyInfo.cs | 36 ++ .../DafnyLanguageService/Resources.Designer.cs | 63 +++ .../Dafny/DafnyLanguageService/Resources.resx | 130 ++++++ .../Dafny/DafnyLanguageService/Resources/Irony.dll | Bin 0 -> 236032 bytes .../Dafny/DafnyLanguageService/VSPackage.resx | 129 ++++++ .../source.extension.vsixmanifest | 27 ++ Util/VS2010/Dafny/StartDafny.bat | 10 + 56 files changed, 4299 insertions(+) create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService.sln create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Key.snk create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx create mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest create mode 100644 Util/VS2010/Chalice/StartChalice.bat create mode 100644 Util/VS2010/Dafny/DafnyLanguageService.sln create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Guids.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Key.snk create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources.resx create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx create mode 100644 Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest create mode 100644 Util/VS2010/Dafny/StartDafny.bat (limited to 'Util/VS2010') diff --git a/Util/VS2010/Chalice/ChaliceLanguageService.sln b/Util/VS2010/Chalice/ChaliceLanguageService.sln new file mode 100644 index 00000000..dfda1244 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService.sln @@ -0,0 +1,20 @@ + +Microsoft Visual Studio Solution File, Format Version 11.00 +# Visual Studio 2010 +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ChaliceLanguageService", "ChaliceLanguageService\ChaliceLanguageService.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/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj b/Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj new file mode 100644 index 00000000..44a36137 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj @@ -0,0 +1,179 @@ + + + + Debug + AnyCPU + 9.0.30729 + 2.0 + Library + Properties + Demo.ChaliceLanguageService + ChaliceLanguageService + 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/Chalice/ChaliceLanguageService/Configuration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs new file mode 100644 index 00000000..8615eee7 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs @@ -0,0 +1,25 @@ +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 = "My C"; +// public const string FormatList = "My C File (*.myc)\n*.myc"; + public const string FormatList = "My C File (*.chalice)\n*.chalice"; + + 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); + } + } +} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs b/Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs new file mode 100644 index 00000000..f0857cbb --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs @@ -0,0 +1,11 @@ +// 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/Chalice/ChaliceLanguageService/Grammar.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs new file mode 100644 index 00000000..56f53c28 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs @@ -0,0 +1,366 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Irony.Parsing; + +namespace Demo +{ + [Language("My C", "1.0", "My C Programming Language")] + public class Grammar : Irony.Parsing.Grammar + { + public Grammar() { + #region 1. Terminals + NumberLiteral n = TerminalFactory.CreateCSharpNumber("number"); + + IdentifierTerminal ident = new IdentifierTerminal("Identifier"); + /* v.AddReservedWords("true", "false", "null", "if", "else", + "while", "for", "foreach", "in", + "switch", "case", "default", "break", + "continue", "return", "function", "is", + "pre", "post", "invariant", "new"); */ + this.MarkReservedWords( + "class", "ghost", "var", "const", "method", "channel", "condition", + "assert", "assume", "new", "this", "reorder", + "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade", + "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned", + "call", "if", "else", "while", + "invariant", "lockchange", + "returns", "requires", "ensures", "where", + "int", "bool", "false", "true", "null", "waitlevel", "lockbottom", + "module", "external", + "predicate", "function", "free", "send", "receive", + "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", + "seq", "nil", "result", "eval", "token", + "wait", "signal" + ); + + 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 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" + | "waitlevel" + | "lockbottom" + | "this" + | "result" + | s + | n + | QualifiedName + // The following is needed: to parse "A=" | "<=" | "is" + | "=" | "+=" | "-=" + | "." + | "==>" | "<==>" | "<<" + ; + + 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 + | "foreach" + LParen + ident + "in" + expression + RParen + Statement + | blockStatement + | expression + Semi + | "break" + Semi + | "continue" + Semi + | "return" + expression + Semi + | QualifiedName + ":=" + Rhs + + | "var" + localVarStmt + | "const" + localVarStmt + + | "call" + identList + ":=" + FunctionExpression + Semi + | "call" + FunctionExpression + Semi + | "assert" + expression + Semi + | "assume" + expression + Semi + | "unshare" + expression + Semi + | "acquire" + expression + Semi + | "release" + expression + Semi + | "downgrade" + expression + Semi + | "free" + expression + Semi + | "fold" + expression + Semi + | "unfold" + expression + Semi + | "reorder" + expression + installBounds + Semi + | "reorder" + expression + Semi + | "share" + expression + installBounds + Semi + | "share" + expression + Semi + | "fork" + identList + ":=" + FunctionExpression + Semi + | "fork" + FunctionExpression + Semi + | "join" + identList + ":=" + expression + Semi + | "join" + expression + Semi + | "send" + expression + Semi + | "receive" + identList + ":=" + expression + Semi + | "receive" + expression + Semi + + ; + Statements.Rule = MakeStarRule(Statements, null, Statement); + blockStatement.Rule = LCurly + Statements + RCurly; + + + #endregion + + #region 3.4 Prog + Prog.Rule = declaration.Star() + Eof; + idType.Rule + = ident + ":" + typeDecl + | ident + ; + + typeDecl.Rule + = (ToTerm("int") | "bool" | ident | "seq") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty) + | ToTerm("token") + "<" + (typeDecl + ".") + ident + ">" + ; + + fieldDecl.Rule + = ToTerm("var") + idType + Semi + | ToTerm("ghost") + "var" + idType + Semi + ; + + methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi; + + formalsList.Rule = MakeStarRule(formalsList, comma, idType); + formalParameters.Rule = LParen + formalsList + RParen; + methodDecl.Rule = "method" + ident + formalParameters + + (("returns" + formalParameters) | Empty) + + methodSpec.Star() + + blockStatement; + functionDecl.Rule + = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}"; + predicateDecl.Rule + = ToTerm("predicate") + ident + "{" + expression + "}"; + invariantDecl.Rule + = ToTerm("invariant") + expression + Semi; + + memberDecl.Rule + = fieldDecl + | invariantDecl + | methodDecl + //| conditionDecl + | predicateDecl + | functionDecl + ; + classDecl.Rule + = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}"; + channelDecl.Rule + = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi + | ToTerm("channel") + ident + formalParameters + Semi; + declaration.Rule = classDecl | channelDecl + ; + + + 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 + RegisterOperators(1, "=", "+=", "-="); + RegisterOperators(2, "+", "-"); + RegisterOperators(3, "*", "/", "%"); + RegisterOperators(4, Associativity.Right, "^"); + RegisterOperators(5, "|", "||"); + RegisterOperators(6, "&", "&&"); + RegisterOperators(7, "==", "!=", ">", "<", ">=", "<=", "<<"); + RegisterOperators(8, "is"); + RegisterOperators(9, "~", "!", "++", "--"); + RegisterOperators(10, "==>", "<==>"); + RegisterOperators(11, "."); + + //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}"); + //RegisterOperators(11, Associativity.Right, "else"); + #endregion + + #region 6. Punctuation symbols + RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";"); + #endregion + } + } +} diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs new file mode 100644 index 00000000..ba02ca8c --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs @@ -0,0 +1,13 @@ +using System; + +namespace Demo +{ + static class GuidList + { + public const string guidIronyLanguageServiceString = "7bcbed0f-df47-4729-b796-b54f14853e2e"; + public const string guidIronyLanguageServicePkgString = "a681f79a-0ed1-4ae0-b79f-4ae69e178800"; + public const string guidIronyLanguageServiceCmdSetString = "be21e7e3-e9c5-4287-95ab-e5125c5063f7"; + + public static readonly Guid guidIronyLanguageServiceCmdSet = new Guid(guidIronyLanguageServiceCmdSetString); + }; +} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs new file mode 100644 index 00000000..9a49dbe4 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs @@ -0,0 +1,66 @@ +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/Chalice/ChaliceLanguageService/Integration/Configuration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs new file mode 100644 index 00000000..f7412393 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs @@ -0,0 +1,116 @@ +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/Chalice/ChaliceLanguageService/Integration/Declaration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs new file mode 100644 index 00000000..c0fda5ca --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs @@ -0,0 +1,30 @@ +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/Chalice/ChaliceLanguageService/Integration/Declarations.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs new file mode 100644 index 00000000..98a411ce --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs @@ -0,0 +1,56 @@ +/*************************************************************************** + +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/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs new file mode 100644 index 00000000..8de1a454 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs @@ -0,0 +1,13 @@ +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/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs new file mode 100644 index 00000000..fd5c4702 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs @@ -0,0 +1,335 @@ +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; + 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 Chalice. + if (!File.Exists(@"C:\tmp\StartChalice.bat")) { + AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartChalice.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\StartChalice.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(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) { + // each line is of the form: "x,y,w,z:arbitrary text" + string[] numbersAndText = line.Split(':'); + if (numbersAndText.Length != 2) { + AddErrorBecauseOfToolProblems(req, "Couldn't find colon in '" + line + "'"); + continue; + } + string numbers = numbersAndText[0]; + var message = numbersAndText[1]; + string[] positions = numbers.Split(','); + if (positions.Length != 4) { + AddErrorBecauseOfToolProblems(req, "Couldn't find four numbers in '" + numbers + "'"); + continue; + } + try { + TextSpan span = new TextSpan(); + span.iStartLine = span.iEndLine = Int32.Parse(positions[0]); + span.iStartIndex = Int32.Parse(positions[1]); + span.iEndLine = Int32.Parse(positions[2]); + span.iEndIndex = Int32.Parse(positions[3]); + req.Sink.AddError(req.FileName, message, span, Severity.Error); + } catch (System.ArgumentNullException) { + AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'"); + } catch (System.FormatException) { + AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'"); + } catch (System.OverflowException) { + AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'"); + } + } + } + } + } + } + + 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 = 1; + span.iStartIndex = 1; + span.iEndIndex = 2; + req.Sink.AddError(req.FileName, msg, span, Severity.Error); + } + + /// + /// 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; + } + } +} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs new file mode 100644 index 00000000..55c3509e --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs @@ -0,0 +1,42 @@ +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/Chalice/ChaliceLanguageService/Integration/LineScanner.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs new file mode 100644 index 00000000..966e9c43 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs @@ -0,0 +1,58 @@ +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/Chalice/ChaliceLanguageService/Integration/Method.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs new file mode 100644 index 00000000..c5071612 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs @@ -0,0 +1,20 @@ +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/Chalice/ChaliceLanguageService/Integration/Methods.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs new file mode 100644 index 00000000..1d7c124f --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs @@ -0,0 +1,50 @@ +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/Chalice/ChaliceLanguageService/Integration/Package.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs new file mode 100644 index 00000000..ae9c00c4 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs @@ -0,0 +1,130 @@ +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 = 1000; + 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/Chalice/ChaliceLanguageService/Integration/Resolver.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs new file mode 100644 index 00000000..9f6ddeba --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs @@ -0,0 +1,50 @@ +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/Chalice/ChaliceLanguageService/Integration/Source.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs new file mode 100644 index 00000000..418bec01 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs @@ -0,0 +1,41 @@ +/*************************************************************************** + +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/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs new file mode 100644 index 00000000..5c475d35 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs @@ -0,0 +1,91 @@ +// 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), ".myc")] + [ProvideLanguageExtension(typeof(IronyLanguageService), ".chalice")] + + // 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", "My C", "Demo", 104)] + [Guid(GuidList.guidIronyLanguageServicePkgString)] + public sealed class MyCLanguageService : 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 MyCLanguageService() + { + 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 + + } +} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Key.snk b/Util/VS2010/Chalice/ChaliceLanguageService/Key.snk new file mode 100644 index 00000000..f80a4ceb Binary files /dev/null and b/Util/VS2010/Chalice/ChaliceLanguageService/Key.snk differ diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..118d4488 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +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/Chalice/ChaliceLanguageService/Resources.Designer.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs new file mode 100644 index 00000000..cd9f79db --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs @@ -0,0 +1,63 @@ +//------------------------------------------------------------------------------ +// +// 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.MyCLanguageService.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/Chalice/ChaliceLanguageService/Resources.resx b/Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx new file mode 100644 index 00000000..03fef612 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx @@ -0,0 +1,130 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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/Chalice/ChaliceLanguageService/Resources/Irony.dll b/Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll new file mode 100644 index 00000000..e2021a72 Binary files /dev/null and b/Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll differ diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx new file mode 100644 index 00000000..c4e76be7 --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx @@ -0,0 +1,129 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 + + + My C + + + My C Programming Language + + \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest b/Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest new file mode 100644 index 00000000..15fd4e9a --- /dev/null +++ b/Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest @@ -0,0 +1,27 @@ + + + + + ChaliceService + Microsoft Research + 1.0 + Information about my package + 1033 + + + + Pro + VST_All + + + + + + + + + + ChaliceService.pkgdef + + + diff --git a/Util/VS2010/Chalice/StartChalice.bat b/Util/VS2010/Chalice/StartChalice.bat new file mode 100644 index 00000000..8e066298 --- /dev/null +++ b/Util/VS2010/Chalice/StartChalice.bat @@ -0,0 +1,10 @@ +@echo off +echo ---------- Starting ------------ < nul >> c:\tmp\coo.out +time < nul >> c:\tmp\coo.out +echo. < nul >> c:\tmp\coo.out + +call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\bin Chalice -nologo -vs -noDeadlockChecks %* 2>> c:\tmp\coo.out + +time < nul >> c:\tmp\coo.out +echo. < nul >> c:\tmp\coo.out +echo ---------- Done ------------ < nul >> c:\tmp\coo.out diff --git a/Util/VS2010/Dafny/DafnyLanguageService.sln b/Util/VS2010/Dafny/DafnyLanguageService.sln new file mode 100644 index 00000000..d900cbb5 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService.sln @@ -0,0 +1,20 @@ + +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 new file mode 100644 index 00000000..f32c75ab --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs @@ -0,0 +1,24 @@ +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 new file mode 100644 index 00000000..175c12dc --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj @@ -0,0 +1,179 @@ + + + + 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 new file mode 100644 index 00000000..f0857cbb --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs @@ -0,0 +1,11 @@ +// 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 new file mode 100644 index 00000000..8853ca9c --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -0,0 +1,445 @@ +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"); + this.MarkReservedWords( + "class", "ghost", "static", "var", "const", "method", "datatype", + "assert", "assume", "new", "this", "object", "refines", "replaces", "by", + "unlimited", "module", "imports", + "call", "if", "then", "else", "while", "invariant", + "break", "label", "return", "foreach", "havoc", "print", "use", + "returns", "requires", "ensures", "modifies", "reads", "decreases", + "int", "bool", "false", "true", "null", + "function", "free", + "in", "forall", "exists", + "seq", "set", "array", + "match", "case", + "fresh", "old" + ); + + 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" + | "=" | "+=" | "-=" + | "." + | "==>" | "<==>" | "<<" + ; + + 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 + | "foreach" + LParen + ident + "in" + expression + RParen + Statement + | blockStatement + | expression + Semi + | "break" + Semi + | "continue" + Semi + | "return" + expression + Semi + | QualifiedName + ":=" + Rhs + + | "var" + localVarStmt + | "const" + localVarStmt + + | "call" + identList + ":=" + FunctionExpression + Semi + | "call" + FunctionExpression + Semi + | "assert" + expression + Semi + | "assume" + expression + Semi + | "unshare" + expression + Semi + | "acquire" + expression + Semi + | "release" + expression + Semi + | "downgrade" + expression + Semi + | "free" + expression + Semi + | "fold" + expression + Semi + | "unfold" + expression + Semi + | "reorder" + expression + installBounds + Semi + | "reorder" + expression + Semi + | "share" + expression + installBounds + Semi + | "share" + expression + Semi + | "fork" + identList + ":=" + FunctionExpression + Semi + | "fork" + FunctionExpression + Semi + | "join" + identList + ":=" + expression + Semi + | "join" + expression + Semi + | "send" + expression + Semi + | "receive" + identList + ":=" + expression + Semi + | "receive" + 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" + | "const" + | "method" + | "datatype" + | "assert" + | "assume" + | "new" + | "this" + | "object" + | "call" + | "if" + | "then" + | "else" + | "while" + | "invariant" + | "break" + | "return" + | "foreach" + | "match" + | "case" + | "returns" + | "requires" + | "ensures" + | "modifies" + | "reads" + | "decreases" + | "int" + | "bool" + | "false" + | "true" + | "null" + | "function" + | "free" + | "in" + | "forall" + | "exists" + | "seq" + | "set" + | "array" + | "match" + | "case" + | "fresh" + | "old" + | ident + | "}" + | "{" + | "(" + | ")" + | "[" + | "]" + | "," + | ":" + | ";" + | "." + | "`" + | "==" + | "!=" + | "<" + | "<=" + | ">=" + | ">" + | "=>" + | ":=" + | "+" + | "-" + | "*" + | "/" + | "%" + | "!!" + | "|" + | "!" + | "&&" + | "||" + | "==>" + | "<==>" + | "#" + | n + ; + + idType.Rule + = ident + ":" + typeDecl + | ident + ; + + typeDecl.Rule + = (ToTerm("int") | "bool" | ident | "seq" | "set" | "array") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty) + | ToTerm("token") + "<" + (typeDecl + ".") + ident + ">" + ; + + fieldDecl.Rule + = ToTerm("var") + idType + Semi + | ToTerm("ghost") + "var" + idType + Semi + ; + + methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi; + + formalsList.Rule = MakeStarRule(formalsList, comma, idType); + formalParameters.Rule = LParen + formalsList + RParen; + methodDecl.Rule = "method" + ident + formalParameters + + (("returns" + formalParameters) | Empty) + + methodSpec.Star() + + blockStatement; + functionDecl.Rule + = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}"; + predicateDecl.Rule + = ToTerm("predicate") + ident + "{" + expression + "}"; + invariantDecl.Rule + = ToTerm("invariant") + expression + Semi; + + memberDecl.Rule + = fieldDecl + | invariantDecl + | methodDecl + //| conditionDecl + | predicateDecl + | functionDecl + ; + classDecl.Rule + = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}"; + channelDecl.Rule + = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi + | ToTerm("channel") + ident + formalParameters + Semi; + declaration.Rule = classDecl | channelDecl + ; + + + 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 + RegisterOperators(1, "<==>"); + RegisterOperators(2, "+", "-"); + RegisterOperators(3, "*", "/", "%", "!!"); + RegisterOperators(4, Associativity.Right, "^"); + RegisterOperators(5, "||"); + RegisterOperators(6, "&&"); + RegisterOperators(7, "==", "!=", ">", "<", ">=", "<="); + RegisterOperators(8, "in"); + RegisterOperators(9, "-", "!", "++", "--"); + RegisterOperators(10, "==>"); + RegisterOperators(11, "."); + + //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}"); + //RegisterOperators(11, Associativity.Right, "else"); + #endregion + + #region 6. Punctuation symbols + RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";"); + #endregion + } + } +} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs b/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs new file mode 100644 index 00000000..61ea05d4 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..9a49dbe4 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs @@ -0,0 +1,66 @@ +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 new file mode 100644 index 00000000..f7412393 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs @@ -0,0 +1,116 @@ +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 new file mode 100644 index 00000000..c0fda5ca --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs @@ -0,0 +1,30 @@ +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 new file mode 100644 index 00000000..98a411ce --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs @@ -0,0 +1,56 @@ +/*************************************************************************** + +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 new file mode 100644 index 00000000..8de1a454 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..aed73699 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs @@ -0,0 +1,343 @@ +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(); !String.IsNullOrEmpty(line); 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" + 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 = 1; + span.iStartIndex = 1; + span.iEndIndex = 2; + req.Sink.AddError(req.FileName, msg, span, Severity.Error); + } + + /// + /// 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 new file mode 100644 index 00000000..55c3509e --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs @@ -0,0 +1,42 @@ +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 new file mode 100644 index 00000000..966e9c43 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs @@ -0,0 +1,58 @@ +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 new file mode 100644 index 00000000..c5071612 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs @@ -0,0 +1,20 @@ +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 new file mode 100644 index 00000000..1d7c124f --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs @@ -0,0 +1,50 @@ +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 new file mode 100644 index 00000000..ae9c00c4 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs @@ -0,0 +1,130 @@ +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 = 1000; + 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 new file mode 100644 index 00000000..9f6ddeba --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs @@ -0,0 +1,50 @@ +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 new file mode 100644 index 00000000..418bec01 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs @@ -0,0 +1,41 @@ +/*************************************************************************** + +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 new file mode 100644 index 00000000..29371f91 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs @@ -0,0 +1,90 @@ +// 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 new file mode 100644 index 00000000..f80a4ceb Binary files /dev/null and b/Util/VS2010/Dafny/DafnyLanguageService/Key.snk differ diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..118d4488 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +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 new file mode 100644 index 00000000..0ca81303 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs @@ -0,0 +1,63 @@ +//------------------------------------------------------------------------------ +// +// 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 new file mode 100644 index 00000000..03fef612 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx @@ -0,0 +1,130 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 new file mode 100644 index 00000000..e2021a72 Binary files /dev/null and b/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll differ diff --git a/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx b/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx new file mode 100644 index 00000000..68782536 --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx @@ -0,0 +1,129 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 new file mode 100644 index 00000000..58e160cd --- /dev/null +++ b/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest @@ -0,0 +1,27 @@ + + + + + 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 new file mode 100644 index 00000000..2313e4d8 --- /dev/null +++ b/Util/VS2010/Dafny/StartDafny.bat @@ -0,0 +1,10 @@ +@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