Source/DafnyMenu/DafnyMenuPackage.cs
/// <summary>
/// Initialization of the package; this method is called right after the package is sited, so this is the place
/// where you can put all the initialization code that rely on services provided by VisualStudio.
/// </summary>
Initialization of the package; this method is called right after the package is sited, so this is the place
where you can put all the initialization code that rely on services provided by VisualStudio.
Initialization of the package ; this method is called right after the package is sited so this is the place where you can put all the initialization code that rely on services provided by VisualStudio .
protected override void Initialize()
    {
      Debug.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString()));
      base.Initialize();
      var mcs = GetService(typeof(IMenuCommandService)) as OleMenuCommandService;
      if (null != mcs)
      {
        var compileCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidCompile);
        compileCommand = new OleMenuCommand(CompileCallback, compileCommandID);
        compileCommand.Enabled = false;
        compileCommand.BeforeQueryStatus += compileCommand_BeforeQueryStatus;
        mcs.AddCommand(compileCommand);
        var runVerifierCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidRunVerifier);
        runVerifierCommand = new OleMenuCommand(RunVerifierCallback, runVerifierCommandID);
        runVerifierCommand.Enabled = true;
        runVerifierCommand.BeforeQueryStatus += runVerifierCommand_BeforeQueryStatus;
        mcs.AddCommand(runVerifierCommand);
        var stopVerifierCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidStopVerifier);
        stopVerifierCommand = new OleMenuCommand(StopVerifierCallback, stopVerifierCommandID);
        stopVerifierCommand.Enabled = true;
        stopVerifierCommand.BeforeQueryStatus += stopVerifierCommand_BeforeQueryStatus;
        mcs.AddCommand(stopVerifierCommand);
        var runResolverCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidRunResolver);
        runResolverCommand = new OleMenuCommand(RunResolverCallback, runResolverCommandID);
        runResolverCommand.Enabled = true;
        runResolverCommand.BeforeQueryStatus += runResolverCommand_BeforeQueryStatus;
        mcs.AddCommand(runResolverCommand);
        var stopResolverCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidStopResolver);
        stopResolverCommand = new OleMenuCommand(StopResolverCallback, stopResolverCommandID);
        stopResolverCommand.Enabled = true;
        stopResolverCommand.BeforeQueryStatus += stopResolverCommand_BeforeQueryStatus;
        mcs.AddCommand(stopResolverCommand);
        var toggleSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleSnapshotVerification);
        toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);
        mcs.AddCommand(toggleSnapshotVerificationCommand);
        var toggleMoreAdvancedSnapshotVerificationCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleMoreAdvancedSnapshotVerification);
        toggleMoreAdvancedSnapshotVerificationCommand = new OleMenuCommand(ToggleMoreAdvancedSnapshotVerificationCallback, toggleMoreAdvancedSnapshotVerificationCommandID);
        toggleMoreAdvancedSnapshotVerificationCommand.Enabled = true;
        toggleMoreAdvancedSnapshotVerificationCommand.BeforeQueryStatus += toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus;
        mcs.AddCommand(toggleMoreAdvancedSnapshotVerificationCommand);
        var toggleAutomaticInductionCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleAutomaticInduction);
        toggleAutomaticInductionCommand = new OleMenuCommand(ToggleAutomaticInductionCallback, toggleAutomaticInductionCommandID);
        toggleAutomaticInductionCommand.Enabled = true;
        toggleAutomaticInductionCommand.BeforeQueryStatus += toggleAutomaticInductionCommand_BeforeQueryStatus;
        mcs.AddCommand(toggleAutomaticInductionCommand);
        var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidToggleBVD);
        toggleBVDCommand = new OleMenuCommand(ToggleBVDCallback, showErrorModelCommandID);
        toggleBVDCommand.Enabled = true;
        toggleBVDCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;
        mcs.AddCommand(toggleBVDCommand);
        var diagnoseTimeoutsCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidDiagnoseTimeouts);
        diagnoseTimeoutsCommand = new OleMenuCommand(DiagnoseTimeoutsCallback, diagnoseTimeoutsCommandID);
        diagnoseTimeoutsCommand.Enabled = true;
        diagnoseTimeoutsCommand.BeforeQueryStatus += diagnoseTimeoutsCommand_BeforeQueryStatus;
        mcs.AddCommand(diagnoseTimeoutsCommand);
        var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);
        menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);
        menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;
        menuCommand.Enabled = true;
        mcs.AddCommand(menuCommand);
      }
    }
protected override void Initialize ( ) { Debug . WriteLine ( string . Format ( CultureInfo . CurrentCulture , " " , this . ToString ( ) ) ) ; base . Initialize ( ) ; var mcs = GetService ( typeof ( IMenuCommandService ) ) as OleMenuCommandService ; if ( null != mcs ) { var compileCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidCompile ) ; compileCommand = new OleMenuCommand ( CompileCallback , compileCommandID ) ; compileCommand . Enabled = false ; compileCommand . BeforeQueryStatus += compileCommand_BeforeQueryStatus ; mcs . AddCommand ( compileCommand ) ; var runVerifierCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidRunVerifier ) ; runVerifierCommand = new OleMenuCommand ( RunVerifierCallback , runVerifierCommandID ) ; runVerifierCommand . Enabled = true ; runVerifierCommand . BeforeQueryStatus += runVerifierCommand_BeforeQueryStatus ; mcs . AddCommand ( runVerifierCommand ) ; var stopVerifierCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidStopVerifier ) ; stopVerifierCommand = new OleMenuCommand ( StopVerifierCallback , stopVerifierCommandID ) ; stopVerifierCommand . Enabled = true ; stopVerifierCommand . BeforeQueryStatus += stopVerifierCommand_BeforeQueryStatus ; mcs . AddCommand ( stopVerifierCommand ) ; var runResolverCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidRunResolver ) ; runResolverCommand = new OleMenuCommand ( RunResolverCallback , runResolverCommandID ) ; runResolverCommand . Enabled = true ; runResolverCommand . BeforeQueryStatus += runResolverCommand_BeforeQueryStatus ; mcs . AddCommand ( runResolverCommand ) ; var stopResolverCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidStopResolver ) ; stopResolverCommand = new OleMenuCommand ( StopResolverCallback , stopResolverCommandID ) ; stopResolverCommand . Enabled = true ; stopResolverCommand . BeforeQueryStatus += stopResolverCommand_BeforeQueryStatus ; mcs . AddCommand ( stopResolverCommand ) ; var toggleSnapshotVerificationCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidToggleSnapshotVerification ) ; toggleSnapshotVerificationCommand = new OleMenuCommand ( ToggleSnapshotVerificationCallback , toggleSnapshotVerificationCommandID ) ; mcs . AddCommand ( toggleSnapshotVerificationCommand ) ; var toggleMoreAdvancedSnapshotVerificationCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidToggleMoreAdvancedSnapshotVerification ) ; toggleMoreAdvancedSnapshotVerificationCommand = new OleMenuCommand ( ToggleMoreAdvancedSnapshotVerificationCallback , toggleMoreAdvancedSnapshotVerificationCommandID ) ; toggleMoreAdvancedSnapshotVerificationCommand . Enabled = true ; toggleMoreAdvancedSnapshotVerificationCommand . BeforeQueryStatus += toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus ; mcs . AddCommand ( toggleMoreAdvancedSnapshotVerificationCommand ) ; var toggleAutomaticInductionCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidToggleAutomaticInduction ) ; toggleAutomaticInductionCommand = new OleMenuCommand ( ToggleAutomaticInductionCallback , toggleAutomaticInductionCommandID ) ; toggleAutomaticInductionCommand . Enabled = true ; toggleAutomaticInductionCommand . BeforeQueryStatus += toggleAutomaticInductionCommand_BeforeQueryStatus ; mcs . AddCommand ( toggleAutomaticInductionCommand ) ; var showErrorModelCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidToggleBVD ) ; toggleBVDCommand = new OleMenuCommand ( ToggleBVDCallback , showErrorModelCommandID ) ; toggleBVDCommand . Enabled = true ; toggleBVDCommand . BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus ; mcs . AddCommand ( toggleBVDCommand ) ; var diagnoseTimeoutsCommandID = new CommandID ( GuidList . guidDafnyMenuCmdSet , ( int ) PkgCmdIDList . cmdidDiagnoseTimeouts ) ; diagnoseTimeoutsCommand = new OleMenuCommand ( DiagnoseTimeoutsCallback , diagnoseTimeoutsCommandID ) ; diagnoseTimeoutsCommand . Enabled = true ; diagnoseTimeoutsCommand . BeforeQueryStatus += diagnoseTimeoutsCommand_BeforeQueryStatus ; mcs . AddCommand ( diagnoseTimeoutsCommand ) ; var menuCommandID = new CommandID ( GuidList . guidDafnyMenuPkgSet , ( int ) PkgCmdIDList . cmdidMenu ) ; menuCommand = new OleMenuCommand ( new EventHandler ( ( sender , e ) => { } ) , menuCommandID ) ; menuCommand . BeforeQueryStatus += menuCommand_BeforeQueryStatus ; menuCommand . Enabled = true ; mcs . AddCommand ( menuCommand ) ; } }
Initialization of the package; this method is called right after the package is sited, so this is the place
where you can put all the initialization code that rely on services provided by VisualStudio.
Initialization of the package ; this method is called right after the package is sited so this is the place where you can put all the initialization code that rely on services provided by VisualStudio .
// Add our command handlers for menu (commands must exist in the .vsct file) // Create the command for the menu item.