001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, 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.dto.module.ConditionalProofVo;
019 import org.qedeq.kernel.xml.common.XmlSyntaxException;
020 import org.qedeq.kernel.xml.handler.common.AbstractSimpleHandler;
021 import org.qedeq.kernel.xml.handler.common.SimpleAttributes;
022
023
024 /**
025 * Parse a conditional proof rule usage.
026 *
027 * @author Michael Meyling
028 */
029 public class ConditionalProofHandler extends AbstractSimpleHandler {
030
031 /** Rule value object. */
032 private ConditionalProofVo conditionalProof;
033
034 /** Handle hypothesis. */
035 private HypothesisHandler hypothesisHandler;
036
037 /** Handle elements. */
038 private FormalProofLineListHandler proofListHandler;
039
040 /** Handle hypothesis. */
041 private ConclusionHandler conclusionHandler;
042
043 /**
044 * Deals with definitions.
045 *
046 * @param handler Parent handler.
047 */
048 public ConditionalProofHandler(final AbstractSimpleHandler handler) {
049 super(handler, "CP");
050 }
051
052 public final void init() {
053 conditionalProof = null;
054 // we initialize the parsers only when really needed (so we have no recursive calls)
055 hypothesisHandler = new HypothesisHandler(this);
056 proofListHandler = new FormalProofLineListHandler(this);
057 conclusionHandler = new ConclusionHandler(this);
058 }
059
060 /**
061 * Get conditional proof usage.
062 *
063 * @return Substitute Free Variable usage.
064 */
065 public final ConditionalProofVo getConditionalProofVo() {
066 return conditionalProof;
067 }
068
069 public final void startElement(final String name, final SimpleAttributes attributes)
070 throws XmlSyntaxException {
071 if (getStartTag().equals(name)) {
072 // ok
073 } else if (hypothesisHandler.getStartTag().equals(name)) {
074 changeHandler(hypothesisHandler, name, attributes);
075 } else if (proofListHandler.getStartTag().equals(name)) {
076 changeHandler(proofListHandler, name, attributes);
077 } else if (conclusionHandler.getStartTag().equals(name)) {
078 changeHandler(conclusionHandler, name, attributes);
079 } else {
080 throw XmlSyntaxException.createUnexpectedTagException(name);
081 }
082 }
083
084 public final void endElement(final String name) throws XmlSyntaxException {
085 if (getStartTag().equals(name)) {
086 conditionalProof = new ConditionalProofVo(hypothesisHandler.getHypothesis(),
087 proofListHandler.getFormalProofLineList(),
088 conclusionHandler.getConclusion());
089 } else if (hypothesisHandler.getStartTag().equals(name)) {
090 // ok
091 } else if (proofListHandler.getStartTag().equals(name)) {
092 // ok
093 } else if (conclusionHandler.getStartTag().equals(name)) {
094 // ok
095 } else {
096 throw XmlSyntaxException.createUnexpectedTagException(name);
097 }
098 }
099
100 }
|