Java 类org.eclipse.jface.text.DocumentRewriteSessionType 实例源码

/**
 * Applies all given changes to the given document. This method assumes that 'changes' contains only changes
 * intended for the given document; the actual URI stored in the changes is ignored.
 */
public void applyAllInSameDocument(Collection<? extends IAtomicChange> changes, IDocument document)
        throws BadLocationException {
    DocumentRewriteSession rewriteSession = null;
    try {
        // prepare
        if (document instanceof IDocumentExtension4) {
            rewriteSession = ((IDocumentExtension4) document).startRewriteSession(
                    DocumentRewriteSessionType.UNRESTRICTED);
        }
        // perform replacements
        for (IAtomicChange currRepl : changes) {
            currRepl.apply(document);
        }
    } finally {
        // cleanup
        if (rewriteSession != null)
            ((IDocumentExtension4) document).stopRewriteSession(rewriteSession);
    }
}

/**
    * Sets text to a document
    * @param document
    * @param message
    * @param append
    * @throws BadLocationException
    * Has to be run from non-UI thread
    */
public static synchronized void setDocumentText(final Document document, final String message,
        final boolean append) {

    UIHelper.runUIAsync(new Runnable() {
        public void run() {
            try {
                DocumentRewriteSession rewriteSession;
                if (append && !isDefaultLabel(document)) {
                    rewriteSession = document.startRewriteSession(DocumentRewriteSessionType.SEQUENTIAL);
                    // append to existing document (0 length is valid and means message is going to be appended)
                    document.replace(document.getLength(), 0, message + ((message.endsWith(CR)) ? EMPTY : CR));
                } else {
                    rewriteSession = document.startRewriteSession(DocumentRewriteSessionType.STRICTLY_SEQUENTIAL);
                    // replace of complete document
                    document.replace(0, document.getLength(), message + ((message.endsWith(CR)) ? EMPTY : CR));
                }
                document.stopRewriteSession(rewriteSession);
            } catch (BadLocationException ignored) {
            }
        }
    });
}

/**
 * Executes the text edits on the given document. Subclasses that override this method should call
 * <code>super.performEdits(document)</code>.
 *
 * @param document the document
 * @return an object representing the undo of the executed edits
 * @exception MalformedTreeException is thrown if the edit tree isn't in a valid state. This
 *     exception is thrown before any edit is executed. So the document is still in its original
 *     state.
 * @exception BadLocationException is thrown if one of the edits in the tree can't be executed.
 *     The state of the document is undefined if this exception is thrown.
 * @since 3.5
 */
protected UndoEdit performEdits(IDocument document)
    throws BadLocationException, MalformedTreeException {
  DocumentRewriteSession session = null;
  try {
    if (document instanceof IDocumentExtension4) {
      session =
          ((IDocumentExtension4) document)
              .startRewriteSession(DocumentRewriteSessionType.UNRESTRICTED);
    }

    LinkedModeModel.closeAllModels(document);
    TextEditProcessor processor = createTextEditProcessor(document, TextEdit.CREATE_UNDO, false);
    return processor.performEdits();

  } finally {
    if (session != null) {
      ((IDocumentExtension4) document).stopRewriteSession(session);
    }
  }
}

protected UndoEdit performEdits(IDocument document) throws BadLocationException, MalformedTreeException {
    DocumentRewriteSession session= null;
    try {
        if (document instanceof IDocumentExtension4) {
            session= ((IDocumentExtension4)document).startRewriteSession(
                DocumentRewriteSessionType.UNRESTRICTED);
        }
        return undoEdit.apply(document);
    } finally {
        if (session != null) {
            ((IDocumentExtension4)document).stopRewriteSession(session);
        }
    }
}

public DocumentRewriteSession startRewriteSession(DocumentRewriteSessionType sessionType) {
  Object lockObject = getLockObject();
  if (lockObject == null) {
    return super.startRewriteSession(sessionType);
  }
  synchronized (lockObject) {
    return super.startRewriteSession(sessionType);
  }
}

private void performChangesInSynchronizationContext(
    final IDocument document, final LinkedList undoList, final boolean preview)
    throws BadLocationException {
  DocumentRewriteSession session = null;
  try {
    if (document instanceof IDocumentExtension4)
      session =
          ((IDocumentExtension4) document)
              .startRewriteSession(DocumentRewriteSessionType.UNRESTRICTED);

    for (final Iterator iterator = fChanges.iterator(); iterator.hasNext(); ) {
      final ComposableBufferChange change = (ComposableBufferChange) iterator.next();

      final UndoEdit edit =
          createTextEditProcessor(
                  change,
                  document,
                  undoList != null ? TextEdit.CREATE_UNDO : TextEdit.NONE,
                  preview)
              .performEdits();
      if (undoList != null) undoList.addFirst(edit);
    }

  } finally {
    if (session != null) ((IDocumentExtension4) document).stopRewriteSession(session);
  }
}

/**
 * Starts a rewrite session (keep things in a single undo/redo)
 */
public static DocumentRewriteSession startWrite(IDocument doc) {
    if (doc instanceof IDocumentExtension4) {
        IDocumentExtension4 d = (IDocumentExtension4) doc;
        return d.startRewriteSession(DocumentRewriteSessionType.UNRESTRICTED);
    }
    return null;
}

public TagBasedTLCOutputIncrementalParser(Model model, int prio, boolean isTraceExplorer, Mode mode, final long size)
  {
// create the document
      document = new LargeTextStoreDocument(size);

      this.analyzer = new TagBasedTLCAnalyzer(document);
      this.source = new CachingTLCOutputSource(model, prio);

      // set up the partitioner
      FastPartitioner partitioner = new FastPartitioner(new TagBasedTLCOutputTokenScanner(),
              TagBasedTLCOutputTokenScanner.CONTENT_TYPES);
      partitioner.connect(document);
      document.setDocumentPartitioner(partitioner);


      // now register the listener, responsible for evaluating the partitioning information
      document.addDocumentPartitioningListener(new TLCOutputPartitionChangeListener(mode));

      /*
       *  Register the process source
       *  
       *  There are two different source registries, one for trace exploration
       *  and one for model checking. The source must be added to the
       *  appropriate registry.
       */
      if (isTraceExplorer)
      {
          TLCOutputSourceRegistry.getTraceExploreSourceRegistry().addTLCOutputSource(this.source);
      } else
      {
        if (mode == Mode.BATCH) {
            // TLC always appends to the document. Therefore, we can tell the
            // document to use a more efficient rewrite mode which reduces the time
            // taken to execute replace operations from minutes and hours to
            // seconds.
        // Its down side is that the ResultPage is only updated when the
        // complete log file is fully parsed, whereas in incremental
        // mode, it (potentially) updates after each line.
            document.startRewriteSession(DocumentRewriteSessionType.STRICTLY_SEQUENTIAL);
        }

          TLCOutputSourceRegistry.getModelCheckSourceRegistry().addTLCOutputSource(this.source);
      }
  }

@Override
public DocumentRewriteSession startRewriteSession(DocumentRewriteSessionType sessionType)
        throws IllegalStateException {
    throw new RuntimeException("not implemented");
}