<commit_before><?xml version="1.0" encoding="UTF-8"?>
<?eclipse version="3.2"?>
<plugin>
   <extension
         point="org.lamport.tla.toolbox.tlc.processOutputSink">
      <sink
            class="org.lamport.tla.toolbox.tool.tlc.output.ParsingTLCOutputSink">
      </sink>
   </extension>
   <extension
         point="org.lamport.tla.toolbox.tlc.processOutputSink">
      <sink
            class="org.lamport.tla.toolbox.tool.tlc.output.ConsoleProcessOutputSink">
      </sink>
   </extension>

	<!-- editors -->
   <extension
         point="org.eclipse.ui.editors">
      <editor
            class="org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor"
            extensions="launch"
            icon="icons/full/choice_sc_obj.gif"
            id="org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor"
            name="Model Editor">
      </editor>
   </extension>
   
   <!-- commands -->
   <extension
         point="org.eclipse.ui.commands">
      <category
            description="Commands contributed by the TLC model checker"
            id="toolbox.tool.tlc.commands.category"
            name="TLC Commands">
      </category>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a new model."
            id="toolbox.tool.tlc.commands.model.new"
            name="New Model...">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.new.param"
               name="specName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a new model for current specification."
            id="toolbox.tool.tlc.commands.model.new.delegate.current"
            name="New Model...">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a new model for selected specification."
            id="toolbox.tool.tlc.commands.model.new.delegate.selected"
            name="New Model...">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Opens existing model for current specification."
            id="toolbox.tool.tlc.commands.model.open"
            name="Open Model...">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.open.param"
               name="modelLaunchName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Deletes existing model."
            id="toolbox.tool.tlc.commands.model.delete"
            name="Delete Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.delete.param"
               name="modelName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a copy of a model."
            id="toolbox.tool.tlc.commands.model.clone"
            name="Clone Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.open.param.modelName"
               name="modelName"
               optional="false">
         </commandParameter>
         <commandParameter
               id="toolbox.tool.tlc.commands.model.open.param.modelCloneName"
               name="modelCloneName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a copy of selected model."
            id="toolbox.tool.tlc.commands.model.clone.delegate"
            name="Clone Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.clone.param.modelName"
               name="Model to be cloned"
               optional="true">
         </commandParameter>
      </command>
      <!-- The difference between this command and the "...delegate" above is, 
      	   that handlers associated to this command are *always* created. This 
      	   is used by the CloneModelContributionItem that is supposed to show
      	   clone model candidates regardless of the enabledWhen expression of
      	   the Toolbox's spec explorer enablement state. -->
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a copy of selected model."
            id="toolbox.tool.tlc.commands.model.clone.delegate.always.enabled"
            name="Clone Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.clone.param.modelName"
               name="Model to be cloned"
               optional="true">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Runs the model checker."
            id="toolbox.tool.tlc.commands.model.run"
            name="Run model checking">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Stops the model checker execution."
            id="toolbox.tool.tlc.commands.model.stop"
            name="Stop model checking">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Repairs corrupted model."
            id="toolbox.tool.tlc.commands.model.repair"
            name="Repair corrupted model">
      </command>
      <command
            id="org.lamport.tla.toolbox.tool.tlc.ui.command1"
            name="lets-create-a-command">
      </command>
      <command
            id="toolbox.tool.tlc.commands.open.tlc.errors"
            name="Open TLC Error View">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            defaultHandler="org.lamport.tla.toolbox.tool.tlc.handlers.OpenSavedModuleHandler"
            id="toolbox.tool.tlc.commands.open.savedModule"
            name="Open Saved Module">
         <commandParameter
               id="toolbox.tool.tlc.commands.open.savedModule.modulePath"
               name="Module Path"
               optional="false">
         </commandParameter>
      </command>
      <command
            description="Open a spec, module or model."
            id="org.lamport.tla.toolbox.openElementSelection"
            name="Filtered open element selection dialog">
      </command>
   </extension>
   
   
   <!-- "TLC Model Checker" menu bar contribution -->
   <extension
         point="org.eclipse.ui.menus">
      <menuContribution
            locationURI="menu:org.eclipse.ui.main.menu?after=toolbox.tools.separator">
         <menu
               id="toolbox.toolmenus.tlc"
               label="TLC Model Checker"
               mnemonic="M"
               tooltip="TLC Model Checker Actions">
            <command
                  commandId="toolbox.tool.tlc.commands.model.new.delegate.current"
                  icon="icons/full/choice_sc_obj.gif"
                  id="toolbox.tool.tlc.modellaunch.new"
                  mnemonic="N">
               <visibleWhen
                     checkEnabled="true">
                  <with
                        variable="activeWorkbenchWindow.activePerspective">
                     <not>
                        <equals
                              value="org.lamport.tla.toolbox.ui.perspective.initial">
                        </equals><commit_msg>[Bug] Change Mnemonic for TLC menu to 'C'. Its old value 'M' collides with the proof Manager.<commit_after><?xml version="1.0" encoding="UTF-8"?>
<?eclipse version="3.2"?>
<plugin>
   <extension
         point="org.lamport.tla.toolbox.tlc.processOutputSink">
      <sink
            class="org.lamport.tla.toolbox.tool.tlc.output.ParsingTLCOutputSink">
      </sink>
   </extension>
   <extension
         point="org.lamport.tla.toolbox.tlc.processOutputSink">
      <sink
            class="org.lamport.tla.toolbox.tool.tlc.output.ConsoleProcessOutputSink">
      </sink>
   </extension>

	<!-- editors -->
   <extension
         point="org.eclipse.ui.editors">
      <editor
            class="org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor"
            extensions="launch"
            icon="icons/full/choice_sc_obj.gif"
            id="org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor"
            name="Model Editor">
      </editor>
   </extension>
   
   <!-- commands -->
   <extension
         point="org.eclipse.ui.commands">
      <category
            description="Commands contributed by the TLC model checker"
            id="toolbox.tool.tlc.commands.category"
            name="TLC Commands">
      </category>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a new model."
            id="toolbox.tool.tlc.commands.model.new"
            name="New Model...">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.new.param"
               name="specName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a new model for current specification."
            id="toolbox.tool.tlc.commands.model.new.delegate.current"
            name="New Model...">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a new model for selected specification."
            id="toolbox.tool.tlc.commands.model.new.delegate.selected"
            name="New Model...">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Opens existing model for current specification."
            id="toolbox.tool.tlc.commands.model.open"
            name="Open Model...">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.open.param"
               name="modelLaunchName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Deletes existing model."
            id="toolbox.tool.tlc.commands.model.delete"
            name="Delete Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.delete.param"
               name="modelName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a copy of a model."
            id="toolbox.tool.tlc.commands.model.clone"
            name="Clone Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.open.param.modelName"
               name="modelName"
               optional="false">
         </commandParameter>
         <commandParameter
               id="toolbox.tool.tlc.commands.model.open.param.modelCloneName"
               name="modelCloneName"
               optional="false">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a copy of selected model."
            id="toolbox.tool.tlc.commands.model.clone.delegate"
            name="Clone Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.clone.param.modelName"
               name="Model to be cloned"
               optional="true">
         </commandParameter>
      </command>
      <!-- The difference between this command and the "...delegate" above is, 
      	   that handlers associated to this command are *always* created. This 
      	   is used by the CloneModelContributionItem that is supposed to show
      	   clone model candidates regardless of the enabledWhen expression of
      	   the Toolbox's spec explorer enablement state. -->
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Creates a copy of selected model."
            id="toolbox.tool.tlc.commands.model.clone.delegate.always.enabled"
            name="Clone Model">
         <commandParameter
               id="toolbox.tool.tlc.commands.model.clone.param.modelName"
               name="Model to be cloned"
               optional="true">
         </commandParameter>
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Runs the model checker."
            id="toolbox.tool.tlc.commands.model.run"
            name="Run model checking">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Stops the model checker execution."
            id="toolbox.tool.tlc.commands.model.stop"
            name="Stop model checking">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            description="Repairs corrupted model."
            id="toolbox.tool.tlc.commands.model.repair"
            name="Repair corrupted model">
      </command>
      <command
            id="org.lamport.tla.toolbox.tool.tlc.ui.command1"
            name="lets-create-a-command">
      </command>
      <command
            id="toolbox.tool.tlc.commands.open.tlc.errors"
            name="Open TLC Error View">
      </command>
      <command
            categoryId="toolbox.tool.tlc.commands.category"
            defaultHandler="org.lamport.tla.toolbox.tool.tlc.handlers.OpenSavedModuleHandler"
            id="toolbox.tool.tlc.commands.open.savedModule"
            name="Open Saved Module">
         <commandParameter
               id="toolbox.tool.tlc.commands.open.savedModule.modulePath"
               name="Module Path"
               optional="false">
         </commandParameter>
      </command>
      <command
            description="Open a spec, module or model."
            id="org.lamport.tla.toolbox.openElementSelection"
            name="Filtered open element selection dialog">
      </command>
   </extension>
   
   
   <!-- "TLC Model Checker" menu bar contribution -->
   <extension
         point="org.eclipse.ui.menus">
      <menuContribution
            locationURI="menu:org.eclipse.ui.main.menu?after=toolbox.tools.separator">
         <menu
               id="toolbox.toolmenus.tlc"
               label="TLC Model Checker"
               mnemonic="C"
               tooltip="TLC Model Checker Actions">
            <command
                  commandId="toolbox.tool.tlc.commands.model.new.delegate.current"
                  icon="icons/full/choice_sc_obj.gif"
                  id="toolbox.tool.tlc.modellaunch.new"
                  mnemonic="N">
               <visibleWhen
                     checkEnabled="true">
                  <with
                        variable="activeWorkbenchWindow.activePerspective">
                     <not>
                        <equals
                              value="org.lamport.tla.toolbox.ui.perspective.initial">
                        </equals>
{'fraction_non_alphanumeric': 0.11415824694921926, 'fraction_numerical': 0.0007872982548222018, 'mean_word_length': 1.8159985220764825, 'pattern_counts': {'":': 0, '<': 159, '<?xml version=': 2, '>': 159, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4930936', 'n_tokens_mistral': 4110, 'n_tokens_neox': 4054, 'n_words': 675}