001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: /*
009: * Created on Apr 17, 2005
010: */
011: package de.uka.ilkd.key.gui.nodeviews;
012:
013: import java.awt.datatransfer.DataFlavor;
014: import java.awt.datatransfer.Transferable;
015: import java.awt.datatransfer.UnsupportedFlavorException;
016: import java.io.IOException;
017:
018: import de.uka.ilkd.key.pp.PosInSequent;
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.proof.ProofSaver;
021:
022: /**
023: * This class in an implementation of the {@link Transferable} interface and
024: * allows to transfer a {@link PosInSequent} object.
025: * It supports to data flavors:
026: * <ul>
027: * <li> {@link PosInSequentTransferable#POS_IN_SEQUENT_TRANSFER} flavor which is
028: * of mime type {@link DataFlavor#javaJVMLocalObjectMimeType}</li>
029: * <li> {@link DataFlavor#stringFlavor} which returns the term described
030: * by the {@link de.uka.ilkd.key.pp.PosInSequent} as a parsable string </li>
031: * </ul>
032: */
033: public class PosInSequentTransferable implements Transferable {
034:
035: public static DataFlavor POS_IN_SEQUENT_TRANSFER;
036: static {
037: try {
038: POS_IN_SEQUENT_TRANSFER = new DataFlavor(
039: DataFlavor.javaJVMLocalObjectMimeType);
040: } catch (ClassNotFoundException e) {
041: // POS_IN_SEQUENT_TRANSFER not supported use
042: // string flavor behaviour
043: e.printStackTrace();
044: }
045: }
046:
047: /** the highlighted position in the sequentview to be transferred */
048: private PosInSequent pis;
049:
050: /** the highlighted term as parseable string */
051: private String stringSelection;
052:
053: /**
054: * creates an instance of this transferable
055: * @param pis the PosInSequent to be transfered
056: * (string flavor only supported if pis denotes a term or formula, not the
057: * complete sequent)
058: */
059: public PosInSequentTransferable(PosInSequent pis, Services serv) {
060: this .pis = pis;
061: if (!pis.isSequent()) {
062: this .stringSelection = ProofSaver.printTerm(
063: pis.getPosInOccurrence().subTerm(), serv)
064: .toString();
065: }
066: }
067:
068: /**
069: * returns the supported flavors of this transferable. These are
070: * currently {@link DataFlavor#stringFlavor} and
071: * {@link PosInSequentTransferable#POS_IN_SEQUENT_TRANSFER}
072: *
073: * @see java.awt.datatransfer.Transferable#getTransferDataFlavors()
074: */
075: public DataFlavor[] getTransferDataFlavors() {
076: return new DataFlavor[] { POS_IN_SEQUENT_TRANSFER,
077: DataFlavor.stringFlavor };
078: }
079:
080: /* (non-Javadoc)
081: * @see java.awt.datatransfer.Transferable#isDataFlavorSupported(java.awt.datatransfer.DataFlavor)
082: */
083: public boolean isDataFlavorSupported(DataFlavor flavor) {
084: return flavor != null
085: && (flavor.equals(POS_IN_SEQUENT_TRANSFER) || flavor
086: .equals(DataFlavor.stringFlavor));
087: }
088:
089: /**
090: * if the flavor is equal to the
091: * {@link PosInSequentTransferable#POS_IN_SEQUENT_TRANSFER} the return data
092: * is of kind {@link PosInSequent}. If the flavor equals
093: * {@link DataFlavor#stringFlavor} the highlighted term is returned as
094: * parsable string.
095: * @throws UnsupportedFlavorException if the flavor is not supported
096: */
097: public Object getTransferData(DataFlavor flavor)
098: throws UnsupportedFlavorException, IOException {
099: if (flavor != null) {
100: if (flavor.equals(POS_IN_SEQUENT_TRANSFER)) {
101: return pis;
102: } else if (flavor.equals(DataFlavor.stringFlavor)) {
103: return stringSelection;
104: }
105: }
106: throw new UnsupportedFlavorException(flavor);
107: }
108:
109: }
|