diff options
Diffstat (limited to 'Util/VS2010/Dafny/DafnyLanguageService/Integration')
13 files changed, 1015 insertions, 0 deletions
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<Declaration> declarations;
+ switch (reason)
+ {
+ case ParseReason.CompleteWord:
+ declarations = resolver.FindCompletions(parseResult, line, col);
+ break;
+ case ParseReason.DisplayMemberList:
+ case ParseReason.MemberSelect:
+ case ParseReason.MemberSelectAndHighlightBraces:
+ declarations = resolver.FindMembers(parseResult, line, col);
+ break;
+ default:
+ throw new ArgumentException("reason");
+ }
+
+ return new Declarations(declarations);
+ }
+
+ // ParseReason.GetMethods
+ public override Microsoft.VisualStudio.Package.Methods GetMethods(int line, int col, string name)
+ {
+ return new Methods(resolver.FindMethods(parseResult, line, col, name));
+ }
+
+ // ParseReason.Goto
+ public override string Goto(VSConstants.VSStd97CmdID cmd, IVsTextView textView, int line, int col, out TextSpan span)
+ {
+ span = new TextSpan();
+ return null;
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs 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<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> colorableItems = new List<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem>();
+
+ public static IList<Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem> ColorableItems
+ {
+ get { return colorableItems; }
+ }
+
+ public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background)
+ {
+ return CreateColor(name, foreground, background, false, false);
+ }
+
+ public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough)
+ {
+ colorableItems.Add(new ColorableItem(name, foreground, background, bold, strikethrough));
+ return (TokenColor)colorableItems.Count;
+ }
+
+ public static void ColorToken(string tokenName, TokenType type, TokenColor color, TokenTriggers trigger)
+ {
+ definitions[tokenName] = new TokenDefinition(type, color, trigger);
+ }
+
+ public static TokenDefinition GetDefinition(string tokenName)
+ {
+ TokenDefinition result;
+ return definitions.TryGetValue(tokenName, out result) ? result : defaultDefinition;
+ }
+
+ private static TokenDefinition defaultDefinition = new TokenDefinition(TokenType.Text, TokenColor.Text, TokenTriggers.None);
+ private static Dictionary<string, TokenDefinition> definitions = new Dictionary<string, TokenDefinition>();
+
+ public struct TokenDefinition
+ {
+ public TokenDefinition(TokenType type, TokenColor color, TokenTriggers triggers)
+ {
+ this.TokenType = type;
+ this.TokenColor = color;
+ this.TokenTriggers = triggers;
+ }
+
+ public TokenType TokenType;
+ public TokenColor TokenColor;
+ public TokenTriggers TokenTriggers;
+ }
+ }
+
+ public class ColorableItem : Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem
+ {
+ private string displayName;
+ private COLORINDEX background;
+ private COLORINDEX foreground;
+ private uint fontFlags = (uint)FONTFLAGS.FF_DEFAULT;
+
+ public ColorableItem(string displayName, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough)
+ {
+ this.displayName = displayName;
+ this.background = background;
+ this.foreground = foreground;
+
+ if (bold)
+ this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_BOLD;
+ if (strikethrough)
+ this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_STRIKETHROUGH;
+ }
+
+ #region IVsColorableItem Members
+ public int GetDefaultColors(COLORINDEX[] piForeground, COLORINDEX[] piBackground)
+ {
+ if (null == piForeground)
+ {
+ throw new ArgumentNullException("piForeground");
+ }
+ if (0 == piForeground.Length)
+ {
+ throw new ArgumentOutOfRangeException("piForeground");
+ }
+ piForeground[0] = foreground;
+
+ if (null == piBackground)
+ {
+ throw new ArgumentNullException("piBackground");
+ }
+ if (0 == piBackground.Length)
+ {
+ throw new ArgumentOutOfRangeException("piBackground");
+ }
+ piBackground[0] = background;
+
+ return Microsoft.VisualStudio.VSConstants.S_OK;
+ }
+
+ public int GetDefaultFontFlags(out uint pdwFontFlags)
+ {
+ pdwFontFlags = this.fontFlags;
+ return Microsoft.VisualStudio.VSConstants.S_OK;
+ }
+
+ public int GetDisplayName(out string pbstrName)
+ {
+ pbstrName = displayName;
+ return Microsoft.VisualStudio.VSConstants.S_OK;
+ }
+ #endregion
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs 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<Declaration>
+ {
+ public Declaration(string description, string displayText, int glyph, string name)
+ {
+ this.Description = description;
+ this.DisplayText = displayText;
+ this.Glyph = glyph;
+ this.Name = name;
+ }
+
+ public string Description;
+ public string DisplayText;
+ public int Glyph;
+ public string Name;
+
+ #region IComparable<Declaration> Members
+
+ public int CompareTo(Declaration other)
+ {
+ return DisplayText.CompareTo(other.DisplayText);
+ }
+
+ #endregion
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs 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<Declaration> declarations;
+ public Declarations(IList<Declaration> declarations)
+ {
+ this.declarations = declarations;
+ }
+
+ public override int GetCount()
+ {
+ return declarations.Count;
+ }
+
+ public override string GetDescription(int index)
+ {
+ return declarations[index].Description;
+ }
+
+ public override string GetDisplayText(int index)
+ {
+ return declarations[index].DisplayText;
+ }
+
+ public override int GetGlyph(int index)
+ {
+ return declarations[index].Glyph;
+ }
+
+ public override string GetName(int index)
+ {
+ if (index >= 0)
+ return declarations[index].Name;
+
+ return null;
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs 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<Declaration> FindCompletions(object result, int line, int col);
+ IList<Declaration> FindMembers(object result, int line, int col);
+ string FindQuickInfo(object result, int line, int col);
+ IList<Method> FindMethods(object result, int line, int col, string name);
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs 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<TextSpan[]>();
+ }
+ source.Braces.Add(new TextSpan[2] { openBrace, closeBrace });
+ }
+
+ if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) {
+ foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) {
+ TextSpan span = new TextSpan();
+ span.iStartLine = span.iEndLine = error.Location.Line - 1;
+ span.iStartIndex = error.Location.Column;
+ span.iEndIndex = error.Location.Position;
+ req.Sink.AddError(req.FileName, error.Message, span, Severity.Error);
+ }
+ } else { // parse looks okay, send it to Dafny.
+ if (!File.Exists(@"C:\tmp\StartDafny.bat")) {
+ AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartDafny.bat");
+ } else {
+
+ // From: http://dotnetperls.com/process-redirect-standard-output
+ // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx)
+ //
+ // Setup the process with the ProcessStartInfo class.
+ //
+ ProcessStartInfo start = new ProcessStartInfo();
+ start.FileName = @"cmd.exe";
+ start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name.
+ start.UseShellExecute = false;
+ start.RedirectStandardInput = true;
+ start.RedirectStandardOutput = true;
+ start.CreateNoWindow = true;
+ //start.WindowStyle = ProcessWindowStyle.Minimized; // need this or else you see the window pop up
+ //
+ // Start the process.
+ //
+ using (Process process = Process.Start(start)) {
+ //
+ // Push the file contents to the new process
+ //
+ StreamWriter myStreamWriter = process.StandardInput;
+ myStreamWriter.WriteLine(req.Text);
+ myStreamWriter.Close();
+ //
+ // Read in all the text from the process with the StreamReader.
+ //
+ using (StreamReader reader = process.StandardOutput) {
+ //string result = reader.ReadToEnd();
+ //Console.Write(result);
+
+ for (string line = reader.ReadLine(); !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);
+ }
+
+ /// <summary>
+ /// Called to determine if the given location can have a breakpoint applied to it.
+ /// </summary>
+ /// <param name="buffer">The IVsTextBuffer object containing the source file.</param>
+ /// <param name="line">The line number where the breakpoint is to be set.</param>
+ /// <param name="col">The offset into the line where the breakpoint is to be set.</param>
+ /// <param name="pCodeSpan">
+ /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the
+ /// breakpoint can be set.
+ /// </param>
+ /// <returns>
+ /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given
+ /// position or returns an error code (the validation is deferred until the debug engine is loaded).
+ /// </returns>
+ /// <remarks>
+ /// <para>
+ /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language
+ /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a
+ /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere
+ /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this
+ /// method but the span must always be set. The example shows how this can be done.
+ /// </para>
+ /// <para>
+ /// Since the language service parses the code, it generally knows what is considered code and what
+ /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine.
+ /// </para>
+ /// <para>
+ /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan.
+ /// The parser examines the specified location and returns a span identifying the code at that
+ /// location. If there is code at the location, the span identifying that code should be passed to
+ /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your
+ /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of
+ /// the AuthoringSink class and returns that span in the pCodeSpan argument.
+ /// </para>
+ /// <para>
+ /// The base method returns E_NOTIMPL.
+ /// </para>
+ /// </remarks>
+ public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan)
+ {
+ // TODO: Add code to not allow breakpoints to be placed on non-code lines.
+ // TODO: Refactor to allow breakpoint locations to span multiple lines.
+ if (pCodeSpan != null)
+ {
+ pCodeSpan[0].iStartLine = line;
+ pCodeSpan[0].iStartIndex = col;
+ pCodeSpan[0].iEndLine = line;
+ pCodeSpan[0].iEndIndex = col;
+ if (buffer != null)
+ {
+ int length;
+ buffer.GetLengthOfLine(line, out length);
+ pCodeSpan[0].iStartIndex = 0;
+ pCodeSpan[0].iEndIndex = length;
+ }
+ return VSConstants.S_OK;
+ }
+ else
+ {
+ return VSConstants.S_FALSE;
+ }
+ }
+
+ public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView)
+ {
+ return new IronyViewFilter(mgr, newView);
+ }
+
+ public override string Name
+ {
+ get { return Configuration.Name; }
+ }
+
+ public override string GetFormatFilterList()
+ {
+ return Configuration.FormatList;
+ }
+ }
+}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs 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<Parameter> Parameters;
+ }
+
+ public struct Parameter
+ {
+ public string Name;
+ public string Display;
+ public string Description;
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs 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<Method> methods;
+ public Methods(IList<Method> methods)
+ {
+ this.methods = methods;
+ }
+
+ public override int GetCount()
+ {
+ return methods.Count;
+ }
+
+ public override string GetName(int index)
+ {
+ return methods[index].Name;
+ }
+
+ public override string GetDescription(int index)
+ {
+ return methods[index].Description;
+ }
+
+ public override string GetType(int index)
+ {
+ return methods[index].Type;
+ }
+
+ public override int GetParameterCount(int index)
+ {
+ return (methods[index].Parameters == null) ? 0 : methods[index].Parameters.Count;
+ }
+
+ public override void GetParameterInfo(int index, int paramIndex, out string name, out string display, out string description)
+ {
+ Parameter parameter = methods[index].Parameters[paramIndex];
+ name = parameter.Name;
+ display = parameter.Display;
+ description = parameter.Description;
+ }
+ }
+}
\ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs 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<Demo.Declaration> FindCompletions(object result, int line, int col)
+ {
+ // Used for intellisense.
+ List<Demo.Declaration> declarations = new List<Demo.Declaration>();
+
+ // Add keywords defined by grammar
+ foreach (KeyTerm key in Configuration.Grammar.KeyTerms.Values)
+ {
+ if(key.OptionIsSet(TermOptions.IsKeyword))
+ {
+ declarations.Add(new Declaration("", key.Name, 206, key.Name));
+ }
+ }
+
+ declarations.Sort();
+ return declarations;
+ }
+
+ public IList<Demo.Declaration> FindMembers(object result, int line, int col)
+ {
+ List<Demo.Declaration> members = new List<Demo.Declaration>();
+
+ return members;
+ }
+
+ public string FindQuickInfo(object result, int line, int col)
+ {
+ return "unknown";
+ }
+
+ public IList<Demo.Method> FindMethods(object result, int line, int col, string name)
+ {
+ return new List<Demo.Method>();
+ }
+
+ #endregion
+ }
+}
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs 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<TextSpan[]> braces;
+ public IList<TextSpan[]> Braces
+ {
+ get { return braces; }
+ set { braces = value; }
+ }
+ }
+}
\ No newline at end of file |