diff options
Diffstat (limited to 'Util/VS2010/Boogie/BoogieLanguageService/Integration')
13 files changed, 1006 insertions, 1006 deletions
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs index 9a49dbe4..b5bc4a0e 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/AuthoringScope.cs @@ -1,66 +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;
- }
- }
+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/Boogie/BoogieLanguageService/Integration/Configuration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs index f7412393..706471da 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Configuration.cs @@ -1,116 +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
- }
+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/Boogie/BoogieLanguageService/Integration/Declaration.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs index c0fda5ca..fa1ac730 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declaration.cs @@ -1,30 +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
- }
+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/Boogie/BoogieLanguageService/Integration/Declarations.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs index 98a411ce..ddda8783 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Declarations.cs @@ -1,56 +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;
- }
- }
+/*************************************************************************** + +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/Boogie/BoogieLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs index 8de1a454..f3ff41f4 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IASTResolver.cs @@ -1,13 +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);
- }
+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/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs index 1d1bdce4..30279078 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs @@ -1,343 +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 Boogie.
- if (!File.Exists(@"C:\tmp\StartBoogie.bat")) {
- AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartBoogie.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\StartBoogie.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;
- }
- }
-}
+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 Boogie. + if (!File.Exists(@"C:\tmp\StartBoogie.bat")) { + AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartBoogie.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\StartBoogie.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/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs index 55c3509e..7c673629 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyViewFilter.cs @@ -1,42 +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);
- }
- }
-}
+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/Boogie/BoogieLanguageService/Integration/LineScanner.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs index 966e9c43..b5fdeb8b 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/LineScanner.cs @@ -1,58 +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);
- }
- }
-}
+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/Boogie/BoogieLanguageService/Integration/Method.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs index c5071612..6b6ba00e 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Method.cs @@ -1,20 +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;
- }
+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/Boogie/BoogieLanguageService/Integration/Methods.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs index 1d7c124f..7ce0bb2b 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Methods.cs @@ -1,50 +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;
- }
- }
+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/Boogie/BoogieLanguageService/Integration/Package.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs index dc1244d6..28762c41 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Package.cs @@ -1,130 +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 = 300;
- int hr = mgr.FRegisterComponent(this, crinfo, out componentID);
- }
-
- return language;
- }
- else
- {
- return null;
- }
- });
-
- // proffer the LanguageService
- (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true);
- }
-
- protected override void Dispose(bool disposing)
- {
- try
- {
- if (componentID != 0)
- {
- IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager;
- if (mgr != null)
- {
- mgr.FRevokeComponent(componentID);
- }
- componentID = 0;
- }
- }
- finally
- {
- base.Dispose(disposing);
- }
- }
-
- #region IOleComponent Members
- public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked)
- {
- return 1;
- }
-
- public int FDoIdle(uint grfidlef)
- {
- IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService;
-
- if (ls != null)
- {
- ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0);
- }
-
- return 0;
- }
-
- public int FPreTranslateMessage(MSG[] pMsg)
- {
- return 0;
- }
-
- public int FQueryTerminate(int fPromptUser)
- {
- return 1;
- }
-
- public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam)
- {
- return 1;
- }
-
- public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved)
- {
- return IntPtr.Zero;
- }
-
- public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved)
- {
- }
-
- public void OnAppActivate(int fActive, uint dwOtherThreadID)
- {
- }
-
- public void OnEnterState(uint uStateID, int fEnter)
- {
- }
-
- public void OnLoseActivation()
- {
- }
-
- public void Terminate()
- {
- }
- #endregion
- }
+using System; +using System.Collections.Generic; +using System.Text; +using System.Runtime.InteropServices; +using Microsoft.VisualStudio.OLE.Interop; +using MPF = Microsoft.VisualStudio.Package; +using System.ComponentModel.Design; + +namespace Demo +{ + public class IronyPackage : Microsoft.VisualStudio.Shell.Package, IOleComponent + { + uint componentID = 0; + public IronyPackage() + { + ServiceCreatorCallback callback = new ServiceCreatorCallback( + delegate(IServiceContainer container, Type serviceType) + { + if (typeof(IronyLanguageService) == serviceType) + { + IronyLanguageService language = new IronyLanguageService(); + language.SetSite(this); + + // register for idle time callbacks + IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; + if (componentID == 0 && mgr != null) + { + OLECRINFO[] crinfo = new OLECRINFO[1]; + crinfo[0].cbSize = (uint)Marshal.SizeOf(typeof(OLECRINFO)); + crinfo[0].grfcrf = (uint)_OLECRF.olecrfNeedIdleTime | + (uint)_OLECRF.olecrfNeedPeriodicIdleTime; + crinfo[0].grfcadvf = (uint)_OLECADVF.olecadvfModal | + (uint)_OLECADVF.olecadvfRedrawOff | + (uint)_OLECADVF.olecadvfWarningsOff; + crinfo[0].uIdleTimeInterval = 300; + int hr = mgr.FRegisterComponent(this, crinfo, out componentID); + } + + return language; + } + else + { + return null; + } + }); + + // proffer the LanguageService + (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true); + } + + protected override void Dispose(bool disposing) + { + try + { + if (componentID != 0) + { + IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; + if (mgr != null) + { + mgr.FRevokeComponent(componentID); + } + componentID = 0; + } + } + finally + { + base.Dispose(disposing); + } + } + + #region IOleComponent Members + public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked) + { + return 1; + } + + public int FDoIdle(uint grfidlef) + { + IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService; + + if (ls != null) + { + ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0); + } + + return 0; + } + + public int FPreTranslateMessage(MSG[] pMsg) + { + return 0; + } + + public int FQueryTerminate(int fPromptUser) + { + return 1; + } + + public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam) + { + return 1; + } + + public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved) + { + return IntPtr.Zero; + } + + public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved) + { + } + + public void OnAppActivate(int fActive, uint dwOtherThreadID) + { + } + + public void OnEnterState(uint uStateID, int fEnter) + { + } + + public void OnLoseActivation() + { + } + + public void Terminate() + { + } + #endregion + } }
\ No newline at end of file diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs index 9f6ddeba..579a8a37 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Resolver.cs @@ -1,50 +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
- }
-}
+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/Boogie/BoogieLanguageService/Integration/Source.cs b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs index 418bec01..92b5a884 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Integration/Source.cs @@ -1,41 +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; }
- }
- }
+/*************************************************************************** + +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 |