/**
 * Returns a document representing the file. Note that
 * this document will not be synchronized with changes to
 * the file. It will simply be a snapshot of the file.
 * 
 * Returns null if unsuccessful.
 * 
 * @param module
 * @return
 */
public static IDocument getDocFromFile(IFile file)
{

    /*
     * We need a file document provider to create
     * the document. After the document is created
     * the file document provider must be disconnected
     * to avoid a memory leak.
     */
    FileDocumentProvider fdp = new FileDocumentProvider();
    FileEditorInput input = new FileEditorInput(file);
    try
    {
        fdp.connect(input);
        return fdp.getDocument(input);
    } catch (CoreException e)
    {
        Activator.getDefault().logError("Error getting document for module " + file, e);
    } finally
    {
        fdp.disconnect(input);
    }
    return null;

}
 

public SourceEditor() {
    setSourceViewerConfiguration(new TextUMLSourceViewerConfiguration(this));
    // set the document provider to create the partitioner
    setDocumentProvider(new FileDocumentProvider() {
        protected IDocument createDocument(Object element) throws CoreException {
            IDocument document = super.createDocument(element);
            if (document != null) {
                // this will create partitions
                IDocumentPartitioner partitioner = new FastPartitioner(new PartitionScanner(),
                        ContentTypes.CONFIGURED_CONTENT_TYPES);
                partitioner.connect(document);
                document.setDocumentPartitioner(partitioner);
            }
            return document;
        }
    });
}
 

public CoverageInformation(final List<IFile> savedTLAFiles) {
	for (final IFile iFile : savedTLAFiles) {
		try {
			final FileDocumentProvider fileDocumentProvider = new FileDocumentProvider();
			final FileEditorInput fei = new FileEditorInput(iFile);
			fileDocumentProvider.connect(fei);
			final IDocument document = fileDocumentProvider.getDocument(fei);
			nameToDocument.put(iFile.getName(), document);
		} catch (final CoreException notExpectedToHappen) {
			notExpectedToHappen.printStackTrace();
		}
	}
}
 

protected Map<TLAMarkerInformationHolder, Hashtable<String, Object>> sany2ToolboxErrors(final IProgressMonitor monitor, final IFile rootModule,
		final Vector<TLAMarkerInformationHolder> detectedErrors) throws CoreException {
	FileEditorInput fileEditorInput = new FileEditorInput(rootModule);
       FileDocumentProvider fileDocumentProvider = new FileDocumentProvider();
       final Map<TLAMarkerInformationHolder, Hashtable<String, Object>> result = new HashMap<>();
       try
       {

           fileDocumentProvider.connect(fileEditorInput);

           // The document for manipulation of the MC.tla file
           IDocument document = fileDocumentProvider.getDocument(fileEditorInput);

           // the find/replace adapter to find texts in the document
           FindReplaceDocumentAdapter searchAdapter = new FindReplaceDocumentAdapter(document);

           for (int i = 0; i < detectedErrors.size(); i++)
           {
               // the holder has the information about the error in the MC file
               TLAMarkerInformationHolder markerHolder = (TLAMarkerInformationHolder) detectedErrors.get(i);
               String message = markerHolder.getMessage();
               if (markerHolder.getModuleName() != null)
               {
                   // the root module is MC.tla
                   if (markerHolder.getModuleName().equals(rootModule.getName()))
                   {
                       int severity = markerHolder.getSeverityError();
                       int[] coordinates = markerHolder.getCoordinates();

                       // find the error cause and install the error marker on the corresponding
                       // field
                       result.put(markerHolder, ModelHelper.createMarkerDescription(rootModule, document, searchAdapter,
                               message, severity, coordinates));
                   } else
                   {
                   	// see getLaunch(...) above
                   	DebugPlugin.getDefault().getLaunchManager().removeLaunch(this.launch);
                   	
                       // the reported error is not pointing to the MC file.
                       throw new CoreException(new Status(IStatus.ERROR, TLCActivator.PLUGIN_ID,
                               "Fatal error during validation of the model. "
                                       + "SANY discovered an error somewhere else than the MC file. "
                                       + "This is a bug. The error message was " + message + " in the module "
                                       + markerHolder.getModuleName()));
                   }
               } else
               {
               	// see getLaunch(...) above
                  	DebugPlugin.getDefault().getLaunchManager().removeLaunch(this.launch);
                  	
                   throw new CoreException(new Status(IStatus.ERROR, TLCActivator.PLUGIN_ID,
                           "Fatal error during validation of the model. "
                                   + "SANY discovered an error somewhere else than the MC file. "
                                   + "This is a bug. The error message was " + message + "."));
               }

           }

       } finally
       {
           /*
            * The document provider is not needed. Always disconnect it to avoid a memory leak.
            * 
            * Keeping it connected only seems to provide synchronization of
            * the document with file changes. That is not necessary in this context.
            */
           fileDocumentProvider.disconnect(fileEditorInput);
           monitor.done();
       }
       return result;
}