From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- .../Integration/IronyLanguageService.cs | 686 ++++++++++----------- 1 file changed, 343 insertions(+), 343 deletions(-) (limited to 'Util/VS2010/Boogie/BoogieLanguageService/Integration/IronyLanguageService.cs') 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(); - } - 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); - } - - /// - /// Called to determine if the given location can have a breakpoint applied to it. - /// - /// The IVsTextBuffer object containing the source file. - /// The line number where the breakpoint is to be set. - /// The offset into the line where the breakpoint is to be set. - /// - /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the - /// breakpoint can be set. - /// - /// - /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given - /// position or returns an error code (the validation is deferred until the debug engine is loaded). - /// - /// - /// - /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language - /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a - /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere - /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this - /// method but the span must always be set. The example shows how this can be done. - /// - /// - /// Since the language service parses the code, it generally knows what is considered code and what - /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine. - /// - /// - /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan. - /// The parser examines the specified location and returns a span identifying the code at that - /// location. If there is code at the location, the span identifying that code should be passed to - /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your - /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of - /// the AuthoringSink class and returns that span in the pCodeSpan argument. - /// - /// - /// The base method returns E_NOTIMPL. - /// - /// - public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan) - { - // TODO: Add code to not allow breakpoints to be placed on non-code lines. - // TODO: Refactor to allow breakpoint locations to span multiple lines. - if (pCodeSpan != null) - { - pCodeSpan[0].iStartLine = line; - pCodeSpan[0].iStartIndex = col; - pCodeSpan[0].iEndLine = line; - pCodeSpan[0].iEndIndex = col; - if (buffer != null) - { - int length; - buffer.GetLengthOfLine(line, out length); - pCodeSpan[0].iStartIndex = 0; - pCodeSpan[0].iEndIndex = length; - } - return VSConstants.S_OK; - } - else - { - return VSConstants.S_FALSE; - } - } - - public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView) - { - return new IronyViewFilter(mgr, newView); - } - - public override string Name - { - get { return Configuration.Name; } - } - - public override string GetFormatFilterList() - { - return Configuration.FormatList; - } - } -} +using System; +using System.Collections.Generic; +using System.Diagnostics; +using Microsoft.VisualStudio; +using Microsoft.VisualStudio.TextManager.Interop; +using Microsoft.VisualStudio.Package; + +using Irony.Parsing; +using Irony.Ast; + +using System.IO; + +namespace Demo +{ + public class IronyLanguageService : Microsoft.VisualStudio.Package.LanguageService + { + private Grammar grammar; + private Parser parser; + private ParsingContext context; + + public IronyLanguageService() + { + grammar = new Grammar(); + parser = new Parser(Configuration.Grammar); + context = new ParsingContext(parser); + } + + + #region Custom Colors + public override int GetColorableItem(int index, out IVsColorableItem item) + { + if (index <= Configuration.ColorableItems.Count) + { + item = Configuration.ColorableItems[index - 1]; + return Microsoft.VisualStudio.VSConstants.S_OK; + } + else + { + throw new ArgumentNullException("index"); + } + } + + public override int GetItemCount(out int count) + { + count = Configuration.ColorableItems.Count; + return Microsoft.VisualStudio.VSConstants.S_OK; + } + #endregion + + #region MPF Accessor and Factory specialisation + private LanguagePreferences preferences; + public override LanguagePreferences GetLanguagePreferences() + { + if (this.preferences == null) + { + this.preferences = new LanguagePreferences(this.Site, + typeof(IronyLanguageService).GUID, + this.Name); + this.preferences.Init(); + } + + return this.preferences; + } + + public override Microsoft.VisualStudio.Package.Source CreateSource(IVsTextLines buffer) + { + return new Source(this, buffer, this.GetColorizer(buffer)); + } + + private IScanner scanner; + public override IScanner GetScanner(IVsTextLines buffer) + { + if (scanner == null) + this.scanner = new LineScanner(grammar); + + return this.scanner; + } + #endregion + + public override void OnIdle(bool periodic) + { + // from IronPythonLanguage sample + // this appears to be necessary to get a parse request with ParseReason = Check? + Source src = (Source)GetSource(this.LastActiveTextView); + if (src != null && src.LastParseTime >= Int32.MaxValue >> 12) + { + src.LastParseTime = 0; + } + base.OnIdle(periodic); + } + + public override Microsoft.VisualStudio.Package.AuthoringScope ParseSource(ParseRequest req) + { + Debug.Print("ParseSource at ({0}:{1}), reason {2}", req.Line, req.Col, req.Reason); + Source source = (Source)this.GetSource(req.FileName); + switch (req.Reason) + { + case ParseReason.Check: + // This is where you perform your syntax highlighting. + // Parse entire source as given in req.Text. + // Store results in the AuthoringScope object. + var parsed = parser.Parse(req.Text, req.FileName); + var root = parsed.Root; + if (root != null) { + + AstNode node = (AstNode)root.AstNode; + source.ParseResult = node; + } + + // Used for brace matching. + TokenStack braces = parser.Context.OpenBraces; + foreach (Token brace in braces) { + if (brace.OtherBrace == null) continue; + TextSpan openBrace = new TextSpan(); + openBrace.iStartLine = brace.Location.Line; + openBrace.iStartIndex = brace.Location.Column; + openBrace.iEndLine = brace.Location.Line; + openBrace.iEndIndex = openBrace.iStartIndex + brace.Length; + + TextSpan closeBrace = new TextSpan(); + closeBrace.iStartLine = brace.OtherBrace.Location.Line; + closeBrace.iStartIndex = brace.OtherBrace.Location.Column; + closeBrace.iEndLine = brace.OtherBrace.Location.Line; + closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length; + + if (source.Braces == null) { + source.Braces = new List(); + } + source.Braces.Add(new TextSpan[2] { openBrace, closeBrace }); + } + + if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) { + foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) { + TextSpan span = new TextSpan(); + span.iStartLine = span.iEndLine = error.Location.Line - 1; + span.iStartIndex = error.Location.Column; + span.iEndIndex = error.Location.Position; + req.Sink.AddError(req.FileName, error.Message, span, Severity.Error); + } + } else { // parse looks okay, send it to 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); + } + + /// + /// Called to determine if the given location can have a breakpoint applied to it. + /// + /// The IVsTextBuffer object containing the source file. + /// The line number where the breakpoint is to be set. + /// The offset into the line where the breakpoint is to be set. + /// + /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the + /// breakpoint can be set. + /// + /// + /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given + /// position or returns an error code (the validation is deferred until the debug engine is loaded). + /// + /// + /// + /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language + /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a + /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere + /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this + /// method but the span must always be set. The example shows how this can be done. + /// + /// + /// Since the language service parses the code, it generally knows what is considered code and what + /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine. + /// + /// + /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan. + /// The parser examines the specified location and returns a span identifying the code at that + /// location. If there is code at the location, the span identifying that code should be passed to + /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your + /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of + /// the AuthoringSink class and returns that span in the pCodeSpan argument. + /// + /// + /// The base method returns E_NOTIMPL. + /// + /// + public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan) + { + // TODO: Add code to not allow breakpoints to be placed on non-code lines. + // TODO: Refactor to allow breakpoint locations to span multiple lines. + if (pCodeSpan != null) + { + pCodeSpan[0].iStartLine = line; + pCodeSpan[0].iStartIndex = col; + pCodeSpan[0].iEndLine = line; + pCodeSpan[0].iEndIndex = col; + if (buffer != null) + { + int length; + buffer.GetLengthOfLine(line, out length); + pCodeSpan[0].iStartIndex = 0; + pCodeSpan[0].iEndIndex = length; + } + return VSConstants.S_OK; + } + else + { + return VSConstants.S_FALSE; + } + } + + public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView) + { + return new IronyViewFilter(mgr, newView); + } + + public override string Name + { + get { return Configuration.Name; } + } + + public override string GetFormatFilterList() + { + return Configuration.FormatList; + } + } +} -- cgit v1.2.3