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.se.dto.module;
017
018 import org.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.module.FormalProof;
020 import org.qedeq.kernel.se.base.module.FormalProofLineList;
021 import org.qedeq.kernel.se.base.module.LatexList;
022
023
024 /**
025 * Contains a formal proof for a proposition.
026 *
027 * @author Michael Meyling
028 */
029 public class FormalProofVo implements FormalProof {
030
031 /** Preceding LaTeX text. This text comes before the formal proof. */
032 private LatexList precedingText;
033
034 /** Proof lines. */
035 private FormalProofLineList formalProofLineList;
036
037 /** Succeeding LaTeX text. This text comes after the formal proof. */
038 private LatexList succeedingText;
039
040 /**
041 * Constructs an empty proof.
042 */
043 public FormalProofVo() {
044 // nothing to do
045 }
046
047 /**
048 * Constructs a proof.
049 *
050 * @param formalProofLines The proof lines.
051 */
052 public FormalProofVo(final FormalProofLineList formalProofLines) {
053 this.formalProofLineList = formalProofLines;
054 }
055
056 /**
057 * Set preceding LaTeX text. This text comes before a formal proof.
058 *
059 * @param precedingText Preceding LaTeX text.
060 */
061 public final void setPrecedingText(final LatexListVo precedingText) {
062 this.precedingText = precedingText;
063 }
064
065 public final LatexList getPrecedingText() {
066 return precedingText;
067 }
068
069 /**
070 * Set proof lines for formal proof.
071 *
072 * @param formalProofLines The proof lines.
073 */
074 public final void setFormalProofLineList(final FormalProofLineList formalProofLines) {
075 this.formalProofLineList = formalProofLines;
076 }
077
078 public final FormalProofLineList getFormalProofLineList() {
079 return formalProofLineList;
080 }
081
082 /**
083 * Set succeeding LaTeX text. This text comes after a formal proof.
084 *
085 * @param succeedingText Succeeding LaTeX text.
086 */
087 public final void setSucceedingText(final LatexListVo succeedingText) {
088 this.succeedingText = succeedingText;
089 }
090
091 public final LatexList getSucceedingText() {
092 return succeedingText;
093 }
094
095 public boolean equals(final Object obj) {
096 if (!(obj instanceof FormalProofVo)) {
097 return false;
098 }
099 final FormalProofVo other = (FormalProofVo) obj;
100 return EqualsUtility.equals(getPrecedingText(), other.getPrecedingText())
101 && EqualsUtility.equals(getFormalProofLineList(), other.getFormalProofLineList())
102 && EqualsUtility.equals(getSucceedingText(), other.getSucceedingText());
103 }
104
105 public int hashCode() {
106 return (getPrecedingText() != null ? getPrecedingText().hashCode() : 0)
107 ^ (getFormalProofLineList() != null ? 2 ^ getFormalProofLineList().hashCode() : 0)
108 ^ (getSucceedingText() != null ? 3 ^ getSucceedingText().hashCode() : 0);
109 }
110
111 public String toString() {
112 final StringBuffer result = new StringBuffer();
113 if (getPrecedingText() != null) {
114 result.append(getPrecedingText());
115 }
116 if (getFormalProofLineList() != null) {
117 result.append("Formal Proof: " + getFormalProofLineList());
118 }
119 if (getSucceedingText() != null) {
120 result.append(getSucceedingText());
121 }
122 return result.toString();
123 }
124
125
126 }
|