<commit_before>package org.lamport.tla.toolbox.spec.nature;

import java.io.File;
import java.util.Map;

import org.eclipse.core.filebuffers.ITextFileBuffer;
import org.eclipse.core.filebuffers.ITextFileBufferManager;
import org.eclipse.core.filebuffers.LocationKind;
import org.eclipse.core.resources.IProject;
import org.eclipse.core.resources.IResource;
import org.eclipse.core.resources.IResourceVisitor;
import org.eclipse.core.resources.IncrementalProjectBuilder;
import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.IPath;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.core.runtime.QualifiedName;
import org.eclipse.core.runtime.Status;
import org.eclipse.jface.text.BadLocationException;
import org.eclipse.jface.text.FindReplaceDocumentAdapter;
import org.eclipse.jface.text.IDocument;
import org.eclipse.jface.text.IRegion;
import org.lamport.tla.toolbox.Activator;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.util.ResourceHelper;
import org.lamport.tla.toolbox.util.pref.IPreferenceConstants;

public class PCalDetectingBuilder extends IncrementalProjectBuilder
{

    public static final String BUILDER_ID = "toolbox.builder.PCalAlgorithmSearchingBuilder";
    private static final String PCAL_ALGORITHM_DEFINITION = "--algorithm";
    private static final String PCAL_FAIR_ALGORITHM_DEFINITION = "--fair";

    private PCalDetectingVisitor visitor = new PCalDetectingVisitor();

    /* (non-Javadoc)
     * @see org.eclipse.core.resources.IncrementalProjectBuilder#build(int, java.util.Map, org.eclipse.core.runtime.IProgressMonitor)
     */
    protected IProject[] build(int kind, @SuppressWarnings("rawtypes") Map args, IProgressMonitor monitor) throws CoreException
    {
        final Spec spec = Activator.getSpecManager().getSpecLoaded();
        if (spec == null)
        {
            return null;
        }

        final IProject project = getProject();

        if (project != spec.getProject())
        {
            // skip the build calls on wrong projects (which are in WS, but not a current spec)
            return null;
        }

        project.accept(visitor);

        // must return null
        return null;
    }

    class PCalDetectingVisitor implements IResourceVisitor
    {
        /* (non-Javadoc)
         * @see org.eclipse.core.resources.IResourceVisitor#visit(org.eclipse.core.resources.IResource)
         */
		public boolean visit(IResource resource) throws CoreException {
			// check for resource existence (WS in-sync or out-of-sync)
			if (!resource.exists() || !new File(resource.getLocation().toOSString()).exists()) {
				return false;
			}
			if (IResource.PROJECT == resource.getType()) {
				return true;
			} else if (IResource.FILE == resource.getType() && ResourceHelper.isModule(resource)) {
				final IDocument document = getDocument(resource.getFullPath(), LocationKind.NORMALIZE);
				final FindReplaceDocumentAdapter searchAdapter = new FindReplaceDocumentAdapter(document);
				try {
					// matchRegion is set non-null iff there is a "--algorithm"
					// or "--fair"
					// string in the file. The "--fair" option added by LL on 6
					// July 2011.
					IRegion matchRegion = searchAdapter.find(0, PCAL_ALGORITHM_DEFINITION, true, true, false, false);
					if (matchRegion == null) {
						matchRegion = searchAdapter.find(0, PCAL_FAIR_ALGORITHM_DEFINITION, true, true, false, false);
					}

					// store the session property
					final QualifiedName key = new QualifiedName(Activator.PLUGIN_ID,
							IPreferenceConstants.CONTAINS_PCAL_ALGORITHM);

					// found a algorithm definition
					if (matchRegion != null) {
						resource.setSessionProperty(key, Boolean.TRUE);
					} else {
						resource.setSessionProperty(key, null);
					}
				} catch (BadLocationException e) {
					// do not swallow exceptions locally
					throw new CoreException(new Status(Status.ERROR, Activator.PLUGIN_ID,
							"Error trying to detect the algorithm", e));
				}
			}
			return false;
		}

		/**
		 * @param resource A {@link IResource} for which the corresponding {@link IDocument} should be received
		 */
		/**
		 * @param resourcePath The {@link IPath} to the {@link IResource} for which an {@link IDocument} should be received
		 * @param locKind The {@link LocationKind} of the {@link IPath}
		 * @return The corresponding {@link IDocument} or null
		 * @throws CoreException If the resource could not successfully be received
		 */
		private IDocument getDocument(final IPath resourcePath, final LocationKind locKind) throws CoreException {
			// connect the buffer manager to the given resource
			// the buffermanager takes care of cleanup/disconnecting 
			final ITextFileBufferManager bufferManager = ITextFileBufferManager.DEFAULT;
			bufferManager.connect(resourcePath, locKind, new NullProgressMonitor());

			// get the text file buf from the manager and receive the document
			final ITextFileBuffer itfb = bufferManager.getTextFileBuffer(resourcePath, locKind);
			return itfb.getDocument();
		}
    }
}
<commit_msg>Fix bug where two specs with identical names end up sharing the same editorcontent so that the second spec shows the text file content of the first.<commit_after>package org.lamport.tla.toolbox.spec.nature;

import java.io.File;
import java.util.Map;

import org.eclipse.core.filebuffers.ITextFileBuffer;
import org.eclipse.core.filebuffers.ITextFileBufferManager;
import org.eclipse.core.filebuffers.LocationKind;
import org.eclipse.core.resources.IProject;
import org.eclipse.core.resources.IResource;
import org.eclipse.core.resources.IResourceVisitor;
import org.eclipse.core.resources.IncrementalProjectBuilder;
import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.IPath;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.core.runtime.QualifiedName;
import org.eclipse.core.runtime.Status;
import org.eclipse.jface.text.BadLocationException;
import org.eclipse.jface.text.FindReplaceDocumentAdapter;
import org.eclipse.jface.text.IDocument;
import org.eclipse.jface.text.IRegion;
import org.lamport.tla.toolbox.Activator;
import org.lamport.tla.toolbox.spec.Spec;
import org.lamport.tla.toolbox.util.ResourceHelper;
import org.lamport.tla.toolbox.util.pref.IPreferenceConstants;

public class PCalDetectingBuilder extends IncrementalProjectBuilder
{

    public static final String BUILDER_ID = "toolbox.builder.PCalAlgorithmSearchingBuilder";
    private static final String PCAL_ALGORITHM_DEFINITION = "--algorithm";
    private static final String PCAL_FAIR_ALGORITHM_DEFINITION = "--fair";

    private PCalDetectingVisitor visitor = new PCalDetectingVisitor();

    /* (non-Javadoc)
     * @see org.eclipse.core.resources.IncrementalProjectBuilder#build(int, java.util.Map, org.eclipse.core.runtime.IProgressMonitor)
     */
    protected IProject[] build(int kind, @SuppressWarnings("rawtypes") Map args, IProgressMonitor monitor) throws CoreException
    {
        final Spec spec = Activator.getSpecManager().getSpecLoaded();
        if (spec == null)
        {
            return null;
        }

        final IProject project = getProject();

        if (project != spec.getProject())
        {
            // skip the build calls on wrong projects (which are in WS, but not a current spec)
            return null;
        }

        project.accept(visitor);

        // must return null
        return null;
    }

    class PCalDetectingVisitor implements IResourceVisitor
    {
        /* (non-Javadoc)
         * @see org.eclipse.core.resources.IResourceVisitor#visit(org.eclipse.core.resources.IResource)
         */
		public boolean visit(IResource resource) throws CoreException {
			// check for resource existence (WS in-sync or out-of-sync)
			if (!resource.exists() || !new File(resource.getLocation().toOSString()).exists()) {
				return false;
			}
			if (IResource.PROJECT == resource.getType()) {
				return true;
			} else if (IResource.FILE == resource.getType() && ResourceHelper.isModule(resource)) {
				final IPath fullPath = resource.getFullPath();
				final IDocument document = getDocument(fullPath, LocationKind.NORMALIZE);
				final FindReplaceDocumentAdapter searchAdapter = new FindReplaceDocumentAdapter(document);
				try {
					// matchRegion is set non-null iff there is a "--algorithm"
					// or "--fair"
					// string in the file. The "--fair" option added by LL on 6
					// July 2011.
					IRegion matchRegion = searchAdapter.find(0, PCAL_ALGORITHM_DEFINITION, true, true, false, false);
					if (matchRegion == null) {
						matchRegion = searchAdapter.find(0, PCAL_FAIR_ALGORITHM_DEFINITION, true, true, false, false);
					}

					// store the session property
					final QualifiedName key = new QualifiedName(Activator.PLUGIN_ID,
							IPreferenceConstants.CONTAINS_PCAL_ALGORITHM);

					// found a algorithm definition
					if (matchRegion != null) {
						resource.setSessionProperty(key, Boolean.TRUE);
					} else {
						resource.setSessionProperty(key, null);
					}
				} catch (BadLocationException e) {
					// do not swallow exceptions locally
					throw new CoreException(new Status(Status.ERROR, Activator.PLUGIN_ID,
							"Error trying to detect the algorithm", e));
				} finally {
					// Release document handle so the ITextFileBufferManager can
					// correctly dispose of the document. Disposing means all
					// consumers of the document disconnect. This is done by
					// reference counting per document.
					// If we don't correctly dispose, subsequent document
					// consumers might get an out dated version from the
					// manager's cache if the document names happen to be
					// identical. This is e.g. the case, when a spec with name
					// "frob" is deleted and recreated with name "frob" in a
					// different file system location.
					final ITextFileBufferManager bufferManager = ITextFileBufferManager.DEFAULT;
					bufferManager.disconnect(fullPath, LocationKind.NORMALIZE, new NullProgressMonitor());
				}
			}
			return false;
		}

		/**
		 * @param resource A {@link IResource} for which the corresponding {@link IDocument} should be received
		 */
		/**
		 * @param resourcePath The {@link IPath} to the {@link IResource} for which an {@link IDocument} should be received
		 * @param locKind The {@link LocationKind} of the {@link IPath}
		 * @return The corresponding {@link IDocument} or null
		 * @throws CoreException If the resource could not successfully be received
		 */
		private IDocument getDocument(final IPath resourcePath, final LocationKind locKind) throws CoreException {
			// connect the buffer manager to the given resource
			// the buffermanager takes care of cleanup/disconnecting 
			final ITextFileBufferManager bufferManager = ITextFileBufferManager.DEFAULT;
			bufferManager.connect(resourcePath, locKind, new NullProgressMonitor());

			// get the text file buf from the manager and receive the document
			final ITextFileBuffer itfb = bufferManager.getTextFileBuffer(resourcePath, locKind);
			return itfb.getDocument();
		}
    }
}

{'fraction_non_alphanumeric': 0.09140066282923426, 'fraction_numerical': 0.001221001221001221, 'mean_word_length': 3.309282224727546, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, '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': '5567716', 'n_tokens_mistral': 3576, 'n_tokens_neox': 3132, 'n_words': 867}