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.PropositionVo;
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 proposition.
026 *
027 * @version $Revision: 1.1 $
028 * @author Michael Meyling
029 */
030 public class PropositionHandler extends AbstractSimpleHandler {
031
032 /** Handler for proposition formula. */
033 private final FormulaHandler formulaHandler;
034
035 /** Handler for rule description. */
036 private final LatexListHandler descriptionHandler;
037
038 /** Handle informal proofs. */
039 private final ProofHandler proofHandler;
040
041 /** Handle formal proofs. */
042 private final FormalProofHandler formalProofHandler;
043
044 /** Proposition value object. */
045 private PropositionVo proposition;
046
047
048 /**
049 * Deals with propositions.
050 *
051 * @param handler Parent handler.
052 */
053 public PropositionHandler(final AbstractSimpleHandler handler) {
054 super(handler, "THEOREM");
055 formulaHandler = new FormulaHandler(this);
056 descriptionHandler = new LatexListHandler(this, "DESCRIPTION");
057 proofHandler = new ProofHandler(this);
058 formalProofHandler = new FormalProofHandler(this);
059 }
060
061 public final void init() {
062 proposition = null;
063 }
064
065 /**
066 * Get proposition.
067 *
068 * @return Proposition.
069 */
070 public final PropositionVo getProposition() {
071 return proposition;
072 }
073
074 public final void startElement(final String name, final SimpleAttributes attributes)
075 throws XmlSyntaxException {
076 if (getStartTag().equals(name)) {
077 proposition = new PropositionVo();
078 } else if (formulaHandler.getStartTag().equals(name)) {
079 changeHandler(formulaHandler, name, attributes);
080 } else if (descriptionHandler.getStartTag().equals(name)) {
081 changeHandler(descriptionHandler, name, attributes);
082 } else if (proofHandler.getStartTag().equals(name)) {
083 changeHandler(proofHandler, name, attributes);
084 } else if (formalProofHandler.getStartTag().equals(name)) {
085 changeHandler(formalProofHandler, name, attributes);
086 } else {
087 throw XmlSyntaxException.createUnexpectedTagException(name);
088 }
089 }
090
091 public final void endElement(final String name) throws XmlSyntaxException {
092 if (getStartTag().equals(name)) {
093 // nothing to do
094 } else if (formulaHandler.getStartTag().equals(name)) {
095 proposition.setFormula(formulaHandler.getFormula());
096 } else if (descriptionHandler.getStartTag().equals(name)) {
097 proposition.setDescription(descriptionHandler.getLatexList());
098 } else if (proofHandler.getStartTag().equals(name)) {
099 proposition.addProof(proofHandler.getProof());
100 } else if (formalProofHandler.getStartTag().equals(name)) {
101 proposition.addFormalProof(formalProofHandler.getProof());
102 } else {
103 throw XmlSyntaxException.createUnexpectedTagException(name);
104 }
105 }
106
107 }
|