001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.xml.handler.module;
017
018 import org.qedeq.kernel.se.base.list.Element;
019 import org.qedeq.kernel.se.base.module.Term;
020 import org.qedeq.kernel.se.dto.module.SubstFuncVo;
021 import org.qedeq.kernel.xml.common.XmlSyntaxException;
022 import org.qedeq.kernel.xml.handler.common.AbstractSimpleHandler;
023 import org.qedeq.kernel.xml.handler.common.SimpleAttributes;
024 import org.qedeq.kernel.xml.handler.list.ElementHandler;
025
026
027 /**
028 * Parse a Substitute Function Variable Rule usage.
029 *
030 * @author Michael Meyling
031 */
032 public class SubstFuncvarHandler extends AbstractSimpleHandler {
033
034 /** Rule value object. */
035 private SubstFuncVo substFunc;
036
037 /** Reference to previously proved formula. */
038 private String ref;
039
040 /** Function variable we want to substitute. */
041 private Element functionVariable;
042
043 /** Replacement term. */
044 private Term substituteTerm;
045
046 /** Handle terms. */
047 private final TermHandler termHandler;
048
049 /** Handle elements. */
050 private final ElementHandler elementHandler;
051
052 /**
053 * Deals with definitions.
054 *
055 * @param handler Parent handler.
056 */
057 public SubstFuncvarHandler(final AbstractSimpleHandler handler) {
058 super(handler, "SUBST_FUNVAR");
059 termHandler = new TermHandler(this);
060 elementHandler = new ElementHandler(this);
061 }
062
063 public final void init() {
064 substFunc = null;
065 substituteTerm = null;
066 functionVariable = null;
067 ref = null;
068 }
069
070 /**
071 * Get Substitute Function Variable Rule usage.
072 *
073 * @return Substitute Free Variable usage.
074 */
075 public final SubstFuncVo getSubstFuncVo() {
076 return substFunc;
077 }
078
079 public final void startElement(final String name, final SimpleAttributes attributes)
080 throws XmlSyntaxException {
081 if (getStartTag().equals(name)) {
082 ref = attributes.getString("ref");
083 } else if ("FUNVAR".equals(name)) {
084 changeHandler(elementHandler, name, attributes);
085 } else if (termHandler.getStartTag().equals(name)) {
086 changeHandler(termHandler, name, attributes);
087 } else {
088 throw XmlSyntaxException.createUnexpectedTagException(name);
089 }
090 }
091
092 public final void endElement(final String name) throws XmlSyntaxException {
093 if (getStartTag().equals(name)) {
094 substFunc = new SubstFuncVo(ref, functionVariable,
095 (substituteTerm != null ? substituteTerm.getElement() : null));
096 } else if ("FUNVAR".equals(name)) {
097 functionVariable = elementHandler.getElement();
098 } else if (termHandler.getStartTag().equals(name)) {
099 substituteTerm = termHandler.getTerm();
100 } else {
101 throw XmlSyntaxException.createUnexpectedTagException(name);
102 }
103 }
104
105 }
|