it.uniroma3.plasm.editors
Class PlasmDocumentProvider

java.lang.Object
  org.eclipse.ui.texteditor.AbstractDocumentProvider
      org.eclipse.ui.editors.text.StorageDocumentProvider
          org.eclipse.ui.editors.text.FileDocumentProvider
              it.uniroma3.plasm.editors.PlasmDocumentProvider

All Implemented Interfaces:

org.eclipse.ui.texteditor.IDocumentProvider, org.eclipse.ui.texteditor.IDocumentProviderExtension, org.eclipse.ui.texteditor.IDocumentProviderExtension2, org.eclipse.ui.texteditor.IDocumentProviderExtension3, org.eclipse.ui.editors.text.IStorageDocumentProvider

public class PlasmDocumentProvider

extends org.eclipse.ui.editors.text.FileDocumentProvider

A standard document manager. This document provider is associated with PLaSM editor and creates the PLaSM partitioner.

Author:

EcT(o)PLaSM Group

Constructor Summary

PlasmDocumentProvider()

Methods inherited from class org.eclipse.ui.editors.text.FileDocumentProvider

getModificationStamp, getSynchronizationStamp, isDeleted, isModifiable, isSynchronized

Methods inherited from class org.eclipse.ui.editors.text.StorageDocumentProvider

getDefaultEncoding, getEncoding, isReadOnly, setEncoding

Methods inherited from class org.eclipse.ui.texteditor.AbstractDocumentProvider

aboutToChange, addElementStateListener, canSaveDocument, changed, connect, disconnect, getAnnotationModel, getDocument, getProgressMonitor, getStatus, isStateValidated, mustSaveDocument, removeElementStateListener, resetDocument, saveDocument, setCanSaveDocument, setProgressMonitor, synchronize, updateStateCache, validateState

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

PlasmDocumentProvider

public PlasmDocumentProvider()