/**
 * @(#) gIntTextDocument.java 19.07.01
 *
 * jfem - a java finite element system
 *
 * Copyright (C) 1999-2001 HS-MD
 * jfem.support@jfem.de
 * www.jfem.de
 *
 * For License information see License.txt
 */

package org.app.gui;

import javax.swing.text.PlainDocument;
import javax.swing.text.BadLocationException;
import javax.swing.text.AttributeSet;

/**
 * description:
 * Wird als Document in der Klasse gTextFieldLong verwendet
 * protected Document createDefaultModel() { gIntTextDocument doc = new gIntTextDocument();
 * doc.addDocumentListener(this); return doc; }
 *
 * @version     1.0  19.07.01
 * @author      Thomas Schmidt, Michael Wilhelem
 * @see         #mvc.gui.gTextField
 * @see         #mvc.gui.gTextField0
 * @see         #mvc.gui.gTextFieldInt
 * @see         #PlainDocument
 */

public class gIntTextDocument extends PlainDocument {
    /**
     * Constructor
     * @return none
     * @param none
     * @exception none
     * @version      1.0
     * @author Thomas Schmidt, Michael Wilhelm FH MD, FB Bauwesen
     * @use Example
     * @see  #mvc.gui.gTextField
     * @see  #mvc.gui.gTextField0
     * @see  #mvc.gui.gTextFieldDouble
     * @see  #PlainDocumentDescription:   Wird als Document in der Klasse gTextFieldDouble verwendet
     */
    public gIntTextDocument() {
    }

    /**
     * insertString
     * @return none
     * @param int offs, String str, AttributeSet a
     * @exception none
     * @version      1.0
     * @author Thomas Schmidt, Michael Wilhelm FH MD, FB Bauwesen
     * @use Example
     * @see #gLongTextDocument
     * @see #gDoubleTextDocument Methode des Interface PlainDocument, für das Einfügen eines String
     * Abfangen, wenn es kein gültiger String ist
     */
    public void insertString(int offs, String str, AttributeSet a) throws BadLocationException {
        if (str == null) {
            return;
        }
        int n = getLength(); // alter Wert
        String oldString = getText(0, getLength());
        // Parameters:
        // beginIndex - the beginning index, inclusive.
        // endIndex - the ending index, exclusive.
        String newString = oldString.substring(0, offs) + str + oldString.substring(offs);
        try {
            Integer.parseInt(newString + "0"); //
            super.insertString(offs, str, a);
        }
        catch (NumberFormatException e) {
        }
    }
}
