View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2    *
3    * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10   * This program is distributed in the hope that it will be useful,
11   * but WITHOUT ANY WARRANTY; without even the implied warranty of
12   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13   * GNU General Public License for more details.
14   */
15  
16  package org.qedeq.kernel.se.dto.module;
17  
18  import org.qedeq.base.utility.EqualsUtility;
19  import org.qedeq.kernel.se.base.module.FormalProof;
20  import org.qedeq.kernel.se.base.module.FormalProofLineList;
21  import org.qedeq.kernel.se.base.module.LatexList;
22  
23  
24  /**
25   * Contains a formal proof for a proposition.
26   *
27   * @author  Michael Meyling
28   */
29  public class FormalProofVo implements FormalProof {
30  
31      /** Preceding LaTeX text. This text comes before the formal proof. */
32      private LatexList precedingText;
33  
34      /** Proof lines. */
35      private FormalProofLineList formalProofLineList;
36  
37      /** Succeeding LaTeX text. This text comes after the formal proof. */
38      private LatexList succeedingText;
39  
40      /**
41       * Constructs an empty proof.
42       */
43      public FormalProofVo() {
44          // nothing to do
45      }
46  
47      /**
48       * Constructs a proof.
49       *
50       * @param   formalProofLines    The proof lines.
51       */
52      public FormalProofVo(final FormalProofLineList formalProofLines) {
53          this.formalProofLineList = formalProofLines;
54      }
55  
56      /**
57       * Set preceding LaTeX text. This text comes before a formal proof.
58       *
59       * @param   precedingText   Preceding LaTeX text.
60       */
61      public final void setPrecedingText(final LatexListVo precedingText) {
62          this.precedingText = precedingText;
63      }
64  
65      public final LatexList getPrecedingText() {
66          return precedingText;
67      }
68  
69      /**
70       * Set proof lines for formal proof.
71       *
72       * @param   formalProofLines    The proof lines.
73       */
74      public final void setFormalProofLineList(final FormalProofLineList formalProofLines) {
75          this.formalProofLineList = formalProofLines;
76      }
77  
78      public final FormalProofLineList getFormalProofLineList() {
79          return formalProofLineList;
80      }
81  
82      /**
83       * Set succeeding LaTeX text. This text comes after a formal proof.
84       *
85       * @param   succeedingText  Succeeding LaTeX text.
86       */
87      public final void setSucceedingText(final LatexListVo succeedingText) {
88          this.succeedingText = succeedingText;
89      }
90  
91      public final LatexList getSucceedingText() {
92          return succeedingText;
93      }
94  
95      public boolean equals(final Object obj) {
96          if (!(obj instanceof FormalProofVo)) {
97              return false;
98          }
99          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 }